English
Under ExpChar L p and PerfectRing L p, the p-radical property of i coincides with IsPRadical i p; thus IsPerfectClosure i p is defined as IsPRadical i p.
Русский
При эксп charakter L p и PerfectRing L p свойство p-радикальности индуктора i совпадает с IsPRadical i p; IsPerfectClosure i p определяется как IsPRadical i p.
LaTeX
$$$\mathrm{IsPerfectClosure}(i,p) \\equiv \\mathrm{IsPRadical}(i,p)$$$
Lean4
/-- If `i : K →+* L` is a `p`-radical ring homomorphism, then it makes `L` a perfect closure
of `K`, if `L` is perfect.
In this case the kernel of `i` is equal to the `p`-nilradical of `K`
(see `IsPerfectClosure.ker_eq`).
Our definition makes it synonymous to `IsPRadical` if `PerfectRing L p` is present. A caveat is
that you need to write `[PerfectRing L p] [IsPerfectClosure i p]`. This is similar to
`PerfectRing` which has `ExpChar` as a prerequisite. -/
@[nolint unusedArguments]
abbrev IsPerfectClosure [ExpChar L p] [PerfectRing L p] :=
IsPRadical i p
