Documentation Verification Report

Classification

📁 Source: Mathlib/FieldTheory/IsAlgClosed/Classification.lean

Statistics

Metric	Count
Definitions `equivOfTranscendenceBasis`	1
Theorems `cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt`, `cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt'`, `cardinal_le_max_transcendence_basis`, `cardinal_le_max_transcendence_basis'`, `isAlgClosure_of_transcendence_basis`, `ringEquiv_of_equiv_of_charZero`, `ringEquiv_of_equiv_of_char_eq`	7
Total	8

IsAlgClosed

Definitions

Name	Category	Theorems
`equivOfTranscendenceBasis` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt` 📖	mathematical	`IsTranscendenceBasis` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Cardinal.aleph0`	`Cardinal.lift`	—	`le_of_not_gt` `not_le_of_gt` `cardinal_le_max_transcendence_basis` `max_le` `le_of_lt` `le_rfl` `le_antisymm` `max_eq_left` `le_max_of_le_right` `max_eq_right` `le_trans` `Cardinal.lift_mk_le` `AlgebraicIndependent.injective` `Cardinal.lift_injective` `Cardinal.lift_lift`
`cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt'` 📖	—	`IsTranscendenceBasis` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Cardinal.aleph0`	—	—	`Cardinal.lift_id` `cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt`
`cardinal_le_max_transcendence_basis` 📖	mathematical	`IsTranscendenceBasis` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Cardinal` `Cardinal.instLE` `Cardinal.lift` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot` `Cardinal.aleph0`	—	`Cardinal.lift_max` `Cardinal.lift_aleph0` `Algebra.IsAlgebraic.cardinalMk_le_max` `Subalgebra.isDomain` `instIsDomain` `Subalgebra.instIsTorsionFree'` `IsAlgClosure.isAlgebraic` `isAlgClosure_of_transcendence_basis` `Cardinal.lift_mk_eq` `Cardinal.lift_umax` `Cardinal.lift_le` `max_le_max` `MvPolynomial.cardinalMk_le_max_lift` `le_rfl` `sup_of_le_left` `Cardinal.lift_lift`
`cardinal_le_max_transcendence_basis'` 📖	mathematical	`IsTranscendenceBasis` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Cardinal` `Cardinal.instLE` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot` `Cardinal.aleph0`	—	`Cardinal.lift_id` `cardinal_le_max_transcendence_basis`
`isAlgClosure_of_transcendence_basis` 📖	mathematical	`IsTranscendenceBasis` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`IsAlgClosure` `Subalgebra` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `Subalgebra.toCommRing` `Subalgebra.toAlgebra` `Semifield.toCommSemiring` `Algebra.id` `Subalgebra.instIsTorsionFree'` `instIsDomain`	—	`Subalgebra.instIsTorsionFree'` `instIsDomain` `IsTranscendenceBasis.isAlgebraic` `RingHom.domain_nontrivial` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`ringEquiv_of_equiv_of_charZero` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Cardinal.aleph0`	`RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Distrib.toAdd`	—	`exists_isTranscendenceBasis` `instFaithfulSMulIntOfCharZero` `Cardinal.aleph0_lt_lift` `Cardinal.lift_mk_eq'` `Cardinal.lift_injective` `cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt` `Int.instNontrivial` `le_of_eq` `Cardinal.mk_int`
`ringEquiv_of_equiv_of_char_eq` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Cardinal.aleph0`	`RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Distrib.toAdd`	—	`CharP.char_is_prime_or_zero` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `ringEquiv_of_equiv_of_charZero` `CharP.charP_to_charZero`

---

← Back to Index