IsPerfectClosure

📁 Source: Mathlib/FieldTheory/IsPerfectClosure.lean

Statistics

Metric	Count
Definitions `IsPRadical`, `IsPerfectClosure`, `equiv`, `liftAux`, `liftEquiv`, `pNilradical`	6
Theorems `comap_pNilradical`, `injective_comp`, `injective_comp_of_pNilradical_eq_bot`, `injective_comp_of_perfect`, `isPurelyInseparable`, `ker_le`, `ker_le'`, `of_id`, `pow_mem`, `pow_mem'`, `trans`, `equiv_apply`, `equiv_comp`, `equiv_comp_apply`, `equiv_comp_equiv`, `equiv_comp_equiv_apply`, `equiv_comp_equiv_apply_eq_self`, `equiv_comp_equiv_eq_id`, `equiv_self`, `equiv_self_apply`, `equiv_symm`, `equiv_symm_apply`, `equiv_symm_toRingHom`, `equiv_toRingHom`, `ker_eq`, `isPRadical`, `isPRadical`, `comp_lift`, `comp_lift_apply`, `liftAux_apply`, `liftAux_id`, `liftAux_id_apply`, `liftAux_self`, `liftAux_self_apply`, `liftEquiv_apply`, `liftEquiv_comp_apply`, `liftEquiv_id`, `liftEquiv_id_apply`, `liftEquiv_symm_apply`, `liftEquiv_trans`, `lift_apply`, `lift_aux`, `lift_comp`, `lift_comp_apply`, `lift_comp_lift`, `lift_comp_lift_apply`, `lift_comp_lift_apply_eq_self`, `lift_comp_lift_eq_id`, `lift_id`, `lift_id_apply`, `lift_lift`, `lift_lift_apply`, `lift_self`, `lift_self_apply`, `pNilradical_eq_bot`, `pNilradical_le_ker_of_perfectRing`, `isPRadical_iff`, `mem_pNilradical`, `pNilradical_eq_bot`, `pNilradical_eq_bot'`, `pNilradical_eq_bot_of_frobenius_inj`, `pNilradical_eq_nilradical`, `pNilradical_le_nilradical`, `pNilradical_one`, `pNilradical_prime`, `pow_expChar_pow_inj_of_pNilradical_eq_bot`, `sub_mem_pNilradical_iff_pow_expChar_pow_eq`	67
Total	73

IsPRadical

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_pNilradical` 📖	mathematical	—	`Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `pNilradical`	—	`le_antisymm` `RingHom.instRingHomClass` `mem_pNilradical` `Ideal.mem_comap` `ker_le` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `pow_add` `pow_mul` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass`
`injective_comp` 📖	mathematical	—	`RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.comp`	—	`injective_comp_of_pNilradical_eq_bot` `bot_unique` `LE.le.trans` `pNilradical_le_nilradical` `Eq.le` `nilradical_eq_zero`
`injective_comp_of_pNilradical_eq_bot` 📖	mathematical	`pNilradical` `CommRing.toCommSemiring` `Bot.bot` `Ideal` `CommSemiring.toSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.comp`	—	`RingHom.ext` `pow_mem` `pow_expChar_pow_inj_of_pNilradical_eq_bot` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`injective_comp_of_perfect` 📖	mathematical	—	`RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.comp`	—	`injective_comp_of_pNilradical_eq_bot` `PerfectRing.pNilradical_eq_bot`
`isPurelyInseparable` 📖	mathematical	—	`IsPurelyInseparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`isPurelyInseparable_iff_pow_mem` `instIsDomain` `pow_mem`
`ker_le` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom` `RingHom.instFunLike` `RingHom.instRingHomClass` `pNilradical`	—	`ker_le'`
`ker_le'` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom` `RingHom.instFunLike` `RingHom.instRingHomClass` `pNilradical`	—	—
`of_id` 📖	mathematical	—	`IsPRadical` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`pow_zero` `pow_one` `RingHom.instRingHomClass` `Ideal.zero_mem`
`pow_mem` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`pow_mem'`
`pow_mem'` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	—
`trans` 📖	mathematical	—	`IsPRadical` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`pow_mem` `RingHom.comp_apply` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `pow_add` `pow_mul` `comap_pNilradical` `ker_le` `RingHom.mem_ker`

IsPerfectClosure

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	13 math math: `equiv_comp_equiv_apply_eq_self`, `equiv_toRingHom`, `equiv_symm`, `equiv_self`, `equiv_comp`, `equiv_self_apply`, `equiv_comp_equiv_eq_id`, `equiv_comp_equiv_apply`, `equiv_apply`, `equiv_comp_apply`, `equiv_symm_apply`, `equiv_comp_equiv`, `equiv_symm_toRingHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equiv_apply` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	`DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equiv` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingEquiv.symm` `iterateFrobeniusEquiv` `RingHom` `RingHom.instFunLike`	—	`PerfectRing.liftAux_apply`
`equiv_comp` 📖	mathematical	—	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `equiv`	—	`RingHom.ext` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `equiv_comp_apply`
`equiv_comp_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equiv` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	—	`PerfectRing.lift_comp_apply`
`equiv_comp_equiv` 📖	mathematical	—	`RingEquiv.trans` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `equiv`	—	`RingEquiv.ext` `equiv_comp_equiv_apply`
`equiv_comp_equiv_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equiv`	—	`PerfectRing.lift_comp_lift_apply`
`equiv_comp_equiv_apply_eq_self` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equiv`	—	`equiv_comp_equiv_apply` `equiv_self_apply`
`equiv_comp_equiv_eq_id` 📖	mathematical	—	`RingEquiv.trans` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `equiv` `RingEquiv.refl`	—	`RingEquiv.ext` `equiv_comp_equiv_apply_eq_self`
`equiv_self` 📖	mathematical	—	`equiv` `RingEquiv.refl` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd`	—	`RingEquiv.ext` `equiv_self_apply`
`equiv_self_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equiv`	—	`PerfectRing.liftAux_self_apply`
`equiv_symm` 📖	mathematical	—	`RingEquiv.symm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `equiv`	—	—
`equiv_symm_apply` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	`DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `equiv` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `iterateFrobeniusEquiv` `RingHom` `RingHom.instFunLike`	—	`equiv_symm` `equiv_apply`
`equiv_symm_toRingHom` 📖	mathematical	—	`RingEquiv.toRingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingEquiv.symm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `equiv` `PerfectRing.lift`	—	—
`equiv_toRingHom` 📖	mathematical	—	`RingEquiv.toRingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `equiv` `PerfectRing.lift`	—	—
`ker_eq` 📖	mathematical	—	`RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `pNilradical`	—	`LE.le.antisymm` `RingHom.instRingHomClass` `IsPRadical.ker_le'` `RingHom.pNilradical_le_ker_of_perfectRing`

IsPurelyInseparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPRadical` 📖	mathematical	—	`IsPRadical` `Semifield.toCommSemiring` `Field.toSemifield` `algebraMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`isPurelyInseparable_iff_pow_mem` `instIsDomain` `bot_le` `RingHom.instRingHomClass` `RingHom.injective_iff_ker_eq_bot` `RingHom.injective` `DivisionRing.isSimpleRing` `EuclideanDomain.toNontrivial`

PerfectClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPRadical` 📖	mathematical	—	`IsPRadical` `PerfectClosure` `CommRing.toCommSemiring` `instCommRing` `of`	—	`induction_on` `expChar_prime` `instCharP` `iterate_frobenius` `RingHom.instRingHomClass` `mk_eq_iff` `zero_def` `of_apply` `RingHom.mem_ker` `mem_pNilradical` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `zero_add`

PerfectRing

Definitions

Name	Category	Theorems
`liftAux` 📖	CompOp	5 math math: `liftAux_self`, `liftAux_id_apply`, `liftAux_self_apply`, `liftAux_id`, `liftAux_apply`
`liftEquiv` 📖	CompOp	6 math math: `liftEquiv_comp_apply`, `liftEquiv_id_apply`, `liftEquiv_apply`, `liftEquiv_trans`, `liftEquiv_symm_apply`, `liftEquiv_id`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_lift` 📖	mathematical	—	`lift` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`IsPRadical.injective_comp_of_perfect` `lift_comp`
`comp_lift_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `lift` `RingHom.comp`	—	`comp_lift`
`liftAux_apply` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	`liftAux` `CommRing.toCommSemiring` `DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `iterateFrobeniusEquiv` `RingHom` `RingHom.instFunLike`	—	`lift_aux` `liftAux.eq_1` `mem_pNilradical` `IsPRadical.ker_le` `RingHom.instRingHomClass` `RingHom.mem_ker` `map_sub` `RingHomClass.toAddMonoidHomClass` `sub_eq_zero` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `pow_mul` `mul_comm` `RingEquiv.injective` `iterateFrobeniusEquiv_add_apply` `RingEquiv.apply_symm_apply` `add_assoc` `add_comm` `iterateFrobeniusEquiv_def` `pow_add` `sub_pow_expChar_pow` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass`
`liftAux_id` 📖	mathematical	—	`liftAux` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsPRadical.of_id` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	`IsPRadical.of_id` `liftAux_id_apply`
`liftAux_id_apply` 📖	mathematical	—	`liftAux` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsPRadical.of_id` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	`lift_aux` `IsPRadical.of_id` `RingHom.id_apply` `liftAux.eq_1` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `iterateFrobenius_def` `iterateFrobeniusEquiv_apply` `RingEquiv.symm_apply_apply`
`liftAux_self` 📖	mathematical	—	`liftAux`	—	`liftAux_self_apply`
`liftAux_self_apply` 📖	mathematical	—	`liftAux`	—	`lift_aux` `liftAux.eq_1` `iterateFrobenius_def` `iterateFrobeniusEquiv_apply` `RingEquiv.symm_apply_apply`
`liftEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `liftEquiv` `lift`	—	—
`liftEquiv_comp_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `liftEquiv` `RingHom.comp`	—	`lift_lift`
`liftEquiv_id` 📖	mathematical	—	`liftEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsPRadical.of_id` `Equiv.refl` `RingHom`	—	`Equiv.ext` `IsPRadical.of_id` `liftEquiv_id_apply`
`liftEquiv_id_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `liftEquiv` `RingHom.id` `IsPRadical.of_id`	—	`lift_id`
`liftEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `liftEquiv` `RingHom.comp`	—	—
`liftEquiv_trans` 📖	mathematical	—	`Equiv.trans` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `liftEquiv` `RingHom.comp`	—	`Equiv.ext` `liftEquiv_comp_apply`
`lift_apply` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `lift` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `iterateFrobeniusEquiv`	—	`liftAux_apply`
`lift_aux` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`IsPRadical.pow_mem`
`lift_comp` 📖	mathematical	—	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `lift`	—	`RingHom.ext` `lift_comp_apply`
`lift_comp_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `lift`	—	`lift_apply` `pow_zero` `pow_one` `iterateFrobeniusEquiv_zero`
`lift_comp_lift` 📖	mathematical	—	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `lift`	—	`IsPRadical.injective_comp_of_perfect` `RingHom.ext` `lift_comp_apply` `lift_comp`
`lift_comp_lift_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `lift`	—	`lift_comp_lift`
`lift_comp_lift_apply_eq_self` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `lift`	—	`lift_comp_lift_apply` `lift_self_apply`
`lift_comp_lift_eq_id` 📖	mathematical	—	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `lift` `RingHom.id`	—	`RingHom.ext` `lift_comp_lift_apply_eq_self`
`lift_id` 📖	mathematical	—	`lift` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsPRadical.of_id`	—	`RingHom.ext` `IsPRadical.of_id` `liftAux_id_apply`
`lift_id_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `lift` `RingHom.id` `IsPRadical.of_id`	—	`liftAux_id_apply`
`lift_lift` 📖	mathematical	—	`lift` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`IsPRadical.injective_comp_of_perfect` `RingHom.comp_assoc` `lift_comp`
`lift_lift_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `lift` `RingHom.comp`	—	`lift_lift`
`lift_self` 📖	mathematical	—	`lift` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`RingHom.ext` `liftAux_self_apply`
`lift_self_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `lift`	—	`liftAux_self_apply`
`pNilradical_eq_bot` 📖	mathematical	—	`pNilradical` `Bot.bot` `Ideal` `CommSemiring.toSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`injective_frobenius`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pNilradical_le_ker_of_perfectRing` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `pNilradical` `ker` `RingHom` `instFunLike` `instRingHomClass`	—	`instRingHomClass` `mem_pNilradical` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingEquiv.symm_apply_apply` `iterateFrobeniusEquiv_apply` `iterateFrobenius_def` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass`

(root)

Definitions

Name	Category	Theorems
`IsPRadical` 📖	CompData	5 math math: `IsPRadical.of_id`, `IsPRadical.trans`, `PerfectClosure.isPRadical`, `isPRadical_iff`, `IsPurelyInseparable.isPRadical`
`IsPerfectClosure` 📖	MathDef	—
`pNilradical` 📖	CompOp	16 math math: `pNilradical_prime`, `sub_mem_pNilradical_iff_pow_expChar_pow_eq`, `IsPerfectClosure.ker_eq`, `pNilradical_eq_bot`, `pNilradical_eq_nilradical`, `IsPRadical.ker_le`, `RingHom.pNilradical_le_ker_of_perfectRing`, `mem_pNilradical`, `PerfectRing.pNilradical_eq_bot`, `IsPRadical.comap_pNilradical`, `pNilradical_one`, `isPRadical_iff`, `pNilradical_eq_bot_of_frobenius_inj`, `IsPRadical.ker_le'`, `pNilradical_eq_bot'`, `pNilradical_le_nilradical`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPRadical_iff` 📖	mathematical	—	`IsPRadical` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid` `Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom.instRingHomClass` `pNilradical`	—	`RingHom.instRingHomClass`
`mem_pNilradical` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `pNilradical` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`pNilradical_eq_nilradical` `LT.lt.le` `pow_add` `MulZeroClass.mul_zero` `pNilradical_eq_bot` `Ideal.mem_bot` `pow_zero` `pow_one` `not_lt` `subsingleton_of_zero_eq_one` `zero_pow` `one_pow`
`pNilradical_eq_bot` 📖	mathematical	—	`pNilradical` `Bot.bot` `Ideal` `CommSemiring.toSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`pNilradical.eq_1`
`pNilradical_eq_bot'` 📖	mathematical	—	`pNilradical` `Bot.bot` `Ideal` `CommSemiring.toSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`pNilradical_eq_bot` `not_lt`
`pNilradical_eq_bot_of_frobenius_inj` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `frobenius`	`pNilradical` `Bot.bot` `Ideal` `CommSemiring.toSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`bot_unique` `mem_pNilradical` `Ideal.mem_bot` `Function.Injective.iterate` `coe_iterateFrobenius` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`pNilradical_eq_nilradical` 📖	mathematical	—	`pNilradical` `nilradical`	—	`pNilradical.eq_1`
`pNilradical_le_nilradical` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `pNilradical` `nilradical`	—	`pNilradical.eq_1` `le_refl`
`pNilradical_one` 📖	mathematical	—	`pNilradical` `Bot.bot` `Ideal` `CommSemiring.toSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`pNilradical_eq_bot'` `Eq.le`
`pNilradical_prime` 📖	mathematical	`Nat.Prime`	`pNilradical` `nilradical`	—	`pNilradical_eq_nilradical` `Nat.Prime.one_lt`
`pow_expChar_pow_inj_of_pNilradical_eq_bot` 📖	mathematical	`pNilradical` `CommRing.toCommSemiring` `Bot.bot` `Ideal` `CommSemiring.toSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instMonoid`	—	`sub_eq_zero` `Ideal.mem_bot` `sub_mem_pNilradical_iff_pow_expChar_pow_eq`
`sub_mem_pNilradical_iff_pow_expChar_pow_eq` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `pNilradical` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`sub_pow_expChar_pow`

---

← Back to Index