PerfectClosure

📁 Source: Mathlib/FieldTheory/PerfectClosure.lean

Statistics

Metric	Count
Definitions `R`, `instAdd`, `instAddCommGroup`, `instCommMonoid`, `instCommRing`, `instDivisionRing`, `instField`, `instInhabited`, `instInv`, `instMul`, `instNeg`, `instZero`, `liftOn`, `mk`, `of`	15
Theorems `sound`, `eq_iff`, `frobenius_mk`, `induction_on`, `instCharP`, `instNontrivialOfIsReduced`, `instPerfectField`, `instPerfectRing`, `instReduced`, `intCast`, `iterate_frobenius_mk`, `liftOn_mk`, `mk_add_mk`, `mk_eq_iff`, `mk_inv`, `mk_mul_mk`, `mk_pow`, `mk_succ_pow`, `mk_surjective`, `mk_zero`, `mk_zero_right`, `natCast`, `natCast_eq_iff`, `neg_mk`, `of_apply`, `one_def`, `quot_mk_eq_mk`, `r_iff`, `zero_def`	29
Total	44

PerfectClosure

Definitions

Name	Category	Theorems
`R` 📖	CompData	2 math math: `quot_mk_eq_mk`, `r_iff`
`instAdd` 📖	CompOp	1 math math: `mk_add_mk`
`instAddCommGroup` 📖	CompOp	—
`instCommMonoid` 📖	CompOp	1 math math: `one_def`
`instCommRing` 📖	CompOp	11 math math: `frobenius_mk`, `instCharP`, `instPerfectRing`, `natCast_eq_iff`, `of_apply`, `intCast`, `isPRadical`, `iterate_frobenius_mk`, `instReduced`, `mk_pow`, `natCast`
`instDivisionRing` 📖	CompOp	—
`instField` 📖	CompOp	1 math math: `instPerfectField`
`instInhabited` 📖	CompOp	—
`instInv` 📖	CompOp	1 math math: `mk_inv`
`instMul` 📖	CompOp	1 math math: `mk_mul_mk`
`instNeg` 📖	CompOp	1 math math: `neg_mk`
`instZero` 📖	CompOp	4 math math: `mk_zero_right`, `zero_def`, `instReduced`, `mk_zero`
`liftOn` 📖	CompOp	1 math math: `liftOn_mk`
`mk` 📖	CompOp	—
`of` 📖	CompOp	3 math math: `of_apply`, `isPRadical`, `iterate_frobenius_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_iff` 📖	mathematical	—	`Nat.iterate` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `frobenius` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`expChar_prime` `mk_eq_iff` `Function.Injective.iterate` `add_comm` `Function.iterate_add`
`frobenius_mk` 📖	mathematical	—	`DFunLike.coe` `RingHom` `PerfectClosure` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `frobenius` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instCharP` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`expChar_prime` `instCharP` `mk_pow`
`induction_on` 📖	—	—	—	—	—
`instCharP` 📖	mathematical	—	`CharP` `PerfectClosure` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing`	—	`CharP.cast_eq_zero_iff` `Nat.cast_zero` `natCast_eq_iff`
`instNontrivialOfIsReduced` 📖	mathematical	—	`Nontrivial` `PerfectClosure`	—	`zero_ne_one` `NeZero.one` `expChar_prime` `eq_iff`
`instPerfectField` 📖	mathematical	—	`PerfectField` `PerfectClosure` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`PerfectRing.toPerfectField` `expChar_prime` `instCharP` `instPerfectRing`
`instPerfectRing` 📖	mathematical	—	`PerfectRing` `PerfectClosure` `CommRing.toCommSemiring` `instCommRing` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCharP`	—	`expChar_prime` `instCharP` `Function.bijective_iff_has_inverse` `induction_on` `mk_succ_pow`
`instReduced` 📖	mathematical	—	`IsReduced` `PerfectClosure` `instZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing`	—	`induction_on` `LT.lt.le` `Nat.Prime.one_lt` `Fact.out` `pow_add` `MulZeroClass.mul_zero` `expChar_prime` `zero_add` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mk_pow` `pow_mul`
`intCast` 📖	mathematical	—	`PerfectClosure` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing`	—	`Int.cast_natCast` `natCast` `Int.cast_negSucc` `Nat.cast_add` `Nat.cast_one` `neg_add_rev`
`iterate_frobenius_mk` 📖	mathematical	—	`Nat.iterate` `PerfectClosure` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `frobenius` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instCharP` `of`	—	`expChar_prime` `instCharP` `Function.iterate_succ_apply` `mk_succ_pow`
`liftOn_mk` 📖	mathematical	—	`liftOn`	—	—
`mk_add_mk` 📖	mathematical	—	`PerfectClosure` `instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Nat.iterate` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `frobenius` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`mk_eq_iff` 📖	mathematical	—	`Nat.iterate` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `frobenius` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`expChar_prime` `Quot.eqvGen_exact` `add_assoc` `Function.iterate_add_apply` `add_comm` `add_left_comm` `R.sound`
`mk_inv` 📖	mathematical	—	`PerfectClosure` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield`	—	—
`mk_mul_mk` 📖	mathematical	—	`PerfectClosure` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Nat.iterate` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `frobenius` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`mk_pow` 📖	mathematical	—	`PerfectClosure` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing`	—	`pow_zero` `one_def` `expChar_prime` `mk_eq_iff` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `pow_succ` `iterate_frobenius` `add_zero` `mul_pow` `mul_assoc`
`mk_succ_pow` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—
`mk_surjective` 📖	mathematical	—	`PerfectClosure`	—	`Quot.mk_surjective`
`mk_zero` 📖	mathematical	—	`Prod.instZero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PerfectClosure` `instZero`	—	—
`mk_zero_right` 📖	mathematical	—	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PerfectClosure` `instZero`	—	`expChar_prime` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`natCast` 📖	mathematical	—	`PerfectClosure` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing`	—	`Nat.cast_zero` `mk_zero_right` `Nat.cast_succ` `expChar_prime` `add_zero` `iterate_map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_natCast`
`natCast_eq_iff` 📖	mathematical	—	`PerfectClosure` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing`	—	`expChar_prime` `mk_eq_iff` `natCast` `zero_add` `Function.iterate_fixed` `map_natCast` `RingHom.instRingHomClass`
`neg_mk` 📖	mathematical	—	`PerfectClosure` `instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	—
`of_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `PerfectClosure` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `of`	—	—
`one_def` 📖	mathematical	—	`PerfectClosure` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instCommMonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`quot_mk_eq_mk` 📖	mathematical	—	`R`	—	—
`r_iff` 📖	mathematical	—	`R` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `frobenius` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`expChar_prime`
`zero_def` 📖	mathematical	—	`PerfectClosure` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—

PerfectClosure.R

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sound` 📖	—	`Nat.iterate` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `frobenius` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	`expChar_prime` `zero_add` `Function.iterate_succ'`

---

← Back to Index