Porting Radical.lean

[seewoo5]

• Most of the statements work for UniqueFactorizationMonoid with normalization (or even without normalization, up to unit), so we may upgrade them first by replacing k[X] with general UniqueFactorizationMonoid
• Leave removing normalization condition as a future work
• Put inside RingTheory/UniqueFactorizationDomain.lean? Or make a new lean file Radical.lean somewhere?

Related:
UniqueFactorizationMonoid in https://github.com/leanprover-community/mathlib4/blob/dfc07f1b6271219de25170e4936fee9443d4234c/Mathlib/RingTheory/UniqueFactorizationDomain.lean#L192
NormalizationMonoid in https://github.com/leanprover-community/mathlib4/blob/dfc07f1b6271219de25170e4936fee9443d4234c/Mathlib/Algebra/GCDMonoid/Basic.lean#L73

[seewoo5]

I think we may need to prove that, principal ideal generated by (our) radical $\mathrm{rad}(a)$ of an element $a$ is equal to the ideal radical (in mathlib) of a principal ideal generated by $a$, to make sure that our definition is compatible with the one in mathlib.

(added) Here's a mathematical proof.

Lemma. $\mathrm{rad}(a)^{n} \in (a)$.

Proof) Maybe coprime induction...

Theorem. $(\text{rad}(a)) = \text{rad}((a))$.

Proof) ($\subseteq$) $b \in (\text{rad}(a)) \Leftrightarrow b = r \cdot \text{rad}(a)$ for some $r \in R$. By lemma, $\text{rad}(a)^{n} \in (a)$ for some $n$, so $b^n =r^n \cdot \text{rad}(a)^{n} \in (a)$.

($\supseteq$) $b \in \text{rad}((a)) \Leftrightarrow b^n = r \cdot a$ for some $n$, $r \in R$. Then $\text{rad}(b) = \text{rad}(b^n) = \text{rad}(r)\cdot \text{rad}(a) \Rightarrow \text{rad}(a) | \text{rad}(b) | b \Rightarrow b \in (\text{rad}(a))$.

[seewoo5]

Related:
leanprover-community/mathlib4#14873
leanprover-community/mathlib4#15331

[seewoo5]

leanprover-community/mathlib4#20468