Documentation Verification Report

Tower

📁 Source: Mathlib/FieldTheory/PurelyInseparable/Tower.lean

Statistics

Metric	Count
Definitions	0
Theorems `finInsepDegree_mul_finInsepDegree_of_isAlgebraic`, `insepDegree_eq_of_isSeparable`, `insepDegree_mul_insepDegree_of_isAlgebraic`, `lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic`, `lift_rank_mul_lift_insepDegree_of_isPurelyInseparable`, `lift_rank_mul_lift_sepDegree_of_isSeparable`, `lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic`, `rank_mul_insepDegree_of_isPurelyInseparable`, `rank_mul_sepDegree_of_isSeparable`, `sepDegree_eq_of_isPurelyInseparable`, `sepDegree_eq_of_isPurelyInseparable_of_isSeparable`, `sepDegree_mul_sepDegree_of_isAlgebraic`, `linearDisjoint_of_isPurelyInseparable_of_isSeparable`, `sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable`, `sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable'`, `map_of_isPurelyInseparable_of_isSeparable`, `map_irreducible_of_isPurelyInseparable`, `map_eq_of_isSeparable_of_isPurelyInseparable`	18
Total	18

Field

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finInsepDegree_mul_finInsepDegree_of_isAlgebraic` 📖	mathematical	—	`finInsepDegree`	—	`map_mul` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `Cardinal.toNat_lift` `lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic`
`insepDegree_eq_of_isSeparable` 📖	mathematical	—	`insepDegree`	—	`insepDegree.eq_1` `separableClosure.eq_restrictScalars_of_isSeparable`
`insepDegree_mul_insepDegree_of_isAlgebraic` 📖	mathematical	—	`Cardinal` `Cardinal.instMul` `insepDegree`	—	`Cardinal.lift_id` `lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic`
`lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic` 📖	mathematical	—	`Cardinal` `Cardinal.instMul` `Cardinal.lift` `insepDegree`	—	`lift_rank_mul_lift_insepDegree_of_isPurelyInseparable` `IntermediateField.isScalarTower_bot` `separableClosure.isPurelyInseparable` `insepDegree_eq_of_isSeparable` `IsScalarTower.left` `IntermediateField.isScalarTower_mid` `separableClosure.isSeparable`
`lift_rank_mul_lift_insepDegree_of_isPurelyInseparable` 📖	mathematical	—	`Cardinal` `Cardinal.instMul` `Cardinal.lift` `Module.rank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `insepDegree`	—	`IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left` `IntermediateField.linearDisjoint_of_isPurelyInseparable_of_isSeparable` `separableClosure.isSeparable` `separableClosure.isAlgebraic` `separableClosure.adjoin_eq_of_isAlgebraic` `Normal.toIsAlgebraic` `IsPurelyInseparable.normal`
`lift_rank_mul_lift_sepDegree_of_isSeparable` 📖	mathematical	—	`Cardinal` `Cardinal.instMul` `Cardinal.lift` `Module.rank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `sepDegree`	—	`sepDegree.eq_1` `separableClosure.eq_restrictScalars_of_isSeparable` `lift_rank_mul_lift_rank` `IsScalarTower.left` `IntermediateField.isScalarTower` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `instIsLocalRing` `Module.Free.of_divisionRing`
`lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic` 📖	mathematical	—	`Cardinal` `Cardinal.instMul` `Cardinal.lift` `sepDegree`	—	`IsScalarTower.left` `lift_rank_mul_lift_sepDegree_of_isSeparable` `IntermediateField.isScalarTower_mid` `separableClosure.isSeparable` `sepDegree_eq_of_isPurelyInseparable` `IntermediateField.isScalarTower_bot` `separableClosure.isPurelyInseparable`
`rank_mul_insepDegree_of_isPurelyInseparable` 📖	mathematical	—	`Cardinal` `Cardinal.instMul` `Module.rank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `insepDegree`	—	`Cardinal.lift_id` `lift_rank_mul_lift_insepDegree_of_isPurelyInseparable`
`rank_mul_sepDegree_of_isSeparable` 📖	mathematical	—	`Cardinal` `Cardinal.instMul` `Module.rank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `sepDegree`	—	`Cardinal.lift_id` `lift_rank_mul_lift_sepDegree_of_isSeparable`
`sepDegree_eq_of_isPurelyInseparable` 📖	mathematical	—	`sepDegree`	—	`IsScalarTower.left` `sepDegree.eq_1` `IsScalarTower.of_algebraMap_eq` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `separableClosure.map_eq_of_separableClosure_eq_bot` `separableClosure.separableClosure_eq_bot` `LinearEquiv.rank_eq` `sepDegree_eq_of_isPurelyInseparable_of_isSeparable` `IntermediateField.isScalarTower` `separableClosure.isSeparable`
`sepDegree_eq_of_isPurelyInseparable_of_isSeparable` 📖	mathematical	—	`sepDegree` `Module.rank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`IsScalarTower.left` `IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic_left` `IntermediateField.linearDisjoint_of_isPurelyInseparable_of_isSeparable` `separableClosure.isSeparable` `separableClosure.isAlgebraic` `IntermediateField.rank_top'` `separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable` `Normal.toIsAlgebraic` `IsPurelyInseparable.normal`
`sepDegree_mul_sepDegree_of_isAlgebraic` 📖	mathematical	—	`Cardinal` `Cardinal.instMul` `sepDegree`	—	`Cardinal.lift_id` `lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic`

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearDisjoint_of_isPurelyInseparable_of_isSeparable` 📖	mathematical	—	`LinearDisjoint`	—	`IsScalarTower.left` `Module.Basis.exists_basis` `LinearDisjoint.of_basis_left` `LinearIndependent.map_of_isPurelyInseparable_of_isSeparable` `minpoly_eq` `Algebra.IsSeparable.isSeparable` `LinearIndependent.map'` `Module.Basis.linearIndependent` `LinearMap.ker_eq_bot_of_injective` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable` 📖	mathematical	—	`Field.sepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `isScalarTower_mid'` `restrictScalars_adjoin_of_algEquiv` `restrictScalars_adjoin` `adjoin.mono` `Set.subset_union_right` `Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic` `isScalarTower` `Normal.toIsAlgebraic` `IsPurelyInseparable.normal` `Cardinal.lift_injective` `one_mul` `Cardinal.lift_one` `IsPurelyInseparable.sepDegree_eq_one` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `Field.sepDegree_mul_sepDegree_of_isAlgebraic` `IsScalarTower.of_algebraMap_eq` `ExpChar.exists` `instIsDomain` `restrictScalars_injective` `extendScalars_restrictScalars` `adjoin_self` `adjoin_adjoin_comm` `isPurelyInseparable_adjoin_iff_pow_mem` `expChar` `IsPurelyInseparable.pow_mem` `IsScalarTower.algebraMap_apply` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.toRingHom_eq_coe` `IsScalarTower.coe_toAlgHom` `mul_one`
`sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable'` 📖	mathematical	—	`Field.sepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `SetLike.coe` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `adjoin_self` `sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable`

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_of_isPurelyInseparable_of_isSeparable` 📖	—	`IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `LinearIndependent` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Semifield.toCommSemiring`	—	—	`ExpChar.exists` `instIsDomain` `linearIndependent_iff` `Finsupp.ext` `LT.lt.ne'` `expChar_pow_pos` `pow_mul` `pow_add` `Finset.le_sup` `pow_mem` `SubsemiringClass.toSubmonoidClass` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Finsupp.notMem_support_iff` `zero_pow` `Mathlib.Tactic.Contrapose.contrapose₂` `injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `map_pow_expChar_pow_of_isSeparable'` `sum_pow_char_pow` `expChar_of_injective_algebraMap` `Finsupp.sum.eq_1` `Finsupp.linearCombination_apply` `Finsupp.onFinset_sum` `zero_smul` `Finset.sum_congr` `Algebra.smul_def` `mul_pow` `IsScalarTower.algebraMap_apply` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `eq_zero_of_pow_eq_zero` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `isPurelyInseparable_iff_pow_mem`

Polynomial.Separable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_irreducible_of_isPurelyInseparable` 📖	mathematical	`Polynomial.Separable` `Semifield.toCommSemiring` `Field.toSemifield` `Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring`	`Polynomial.map` `CommSemiring.toSemiring` `algebraMap`	—	`IsAlgClosed.exists_aeval_eq_zero` `AlgebraicClosure.isAlgClosed` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `LT.lt.ne'` `Polynomial.natDegree_pos_iff_degree_pos` `Irreducible.natDegree_pos` `Polynomial.isUnit_C` `IsUnit.inv` `Ne.isUnit` `Polynomial.leadingCoeff_ne_zero` `Irreducible.ne_zero` `IsUnit.unit_spec` `minpoly.eq_of_irreducible` `Associated.map` `MonoidHom.instMonoidHomClass` `minpoly.map_eq_of_isSeparable_of_isPurelyInseparable` `AlgebraicClosure.instIsScalarTower` `IsScalarTower.right` `Associated.separable` `Associated.irreducible_iff` `minpoly.irreducible` `instIsDomain` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `AlgebraicClosure.isAlgebraic`

minpoly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_eq_of_isSeparable_of_isPurelyInseparable` 📖	mathematical	`IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `algebraMap` `minpoly`	—	`IsSeparable.isIntegral` `IsIntegral.tower_top` `Polynomial.eq_of_monic_of_dvd_of_natDegree_le` `monic` `Polynomial.Monic.map` `dvd_map_of_isScalarTower` `le_of_eq` `IsSeparable.tower_top` `IsScalarTower.left` `Algebra.IsSeparable.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IntermediateField.isSeparable_adjoin_simple_iff_isSeparable` `Polynomial.natDegree_map` `DivisionRing.isSimpleRing` `IntermediateField.adjoin.finrank` `Field.finSepDegree_eq_finrank_of_isSeparable` `Field.finSepDegree_eq` `IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable`

---

← Back to Index