Documentation Verification Report

EssentialFiniteness

📁 Source: Mathlib/RingTheory/EssentialFiniteness.lean

Statistics

Metric	Count
Definitions `finset`, `subalgebra`, `submonoid`, `finset`	4
Theorems `adjoin_mem_finset`, `algHom_ext`, `aux`, `baseChange`, `comp`, `comp_iff`, `cond`, `iff_of_algEquiv`, `isLocalization`, `of_comp`, `of_finiteType`, `of_id`, `of_isLocalization`, `of_surjective`, `essFiniteType_cond_iff`, `essFiniteType_iff`, `essFiniteType_iff_exists_subalgebra`, `instEssFiniteTypeLocalization`, `instEssFiniteTypeQuotientIdeal`, `instFiniteTypeSubtypeMemSubalgebraSubalgebra`, `ext`, `essFiniteType`, `essFiniteType_algebraMap`	23
Total	27

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`essFiniteType_cond_iff` 📖	mathematical	—	`IsLocalization` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `adjoin` `SetLike.coe` `Finset` `Finset.instSetLike` `Subalgebra.toCommSemiring` `Submonoid.comap` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `Subalgebra.toSemiring` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `algebraMap` `Subalgebra.toAlgebra` `id` `IsUnit.submonoid` `IsUnit` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Submonoid.IsLocalizationMap.surj` `IsLocalization'.toIsLocalizationMap` `Subtype.prop` `one_mul`
`essFiniteType_iff` 📖	mathematical	—	`EssFiniteType` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `adjoin` `SetLike.coe` `Finset` `Finset.instSetLike` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`essFiniteType_iff_exists_subalgebra` 📖	mathematical	—	`EssFiniteType` `FiniteType` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Subalgebra.toSemiring` `Subalgebra.algebra` `IsLocalization` `Subalgebra.toCommSemiring` `Subalgebra.toAlgebra` `id`	—	`instFiniteTypeSubtypeMemSubalgebraSubalgebra` `EssFiniteType.isLocalization` `EssFiniteType.comp` `IsScalarTower.subalgebra'` `IsScalarTower.right` `EssFiniteType.of_finiteType` `EssFiniteType.of_isLocalization`
`instEssFiniteTypeLocalization` 📖	mathematical	—	`EssFiniteType` `Localization` `CommRing.toCommMonoid` `OreLocalization.instCommRing` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`EssFiniteType.of_isLocalization` `Localization.isLocalization` `EssFiniteType.comp` `OreLocalization.instIsScalarTower` `IsScalarTower.right`
`instEssFiniteTypeQuotientIdeal` 📖	mathematical	—	`EssFiniteType` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.Quotient.commRing` `Ideal.instAlgebraQuotient`	—	`EssFiniteType.comp` `Ideal.Quotient.isScalarTower` `IsScalarTower.right` `EssFiniteType.of_finiteType` `FiniteType.quotient` `Module.Finite.finiteType` `Module.Finite.self`
`instFiniteTypeSubtypeMemSubalgebraSubalgebra` 📖	mathematical	—	`FiniteType` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `EssFiniteType.subalgebra` `Subalgebra.toSemiring` `Subalgebra.algebra`	—	`Subalgebra.fg_top` `EssFiniteType.subalgebra.eq_1`

Algebra.EssFiniteType

Definitions

Name	Category	Theorems
`finset` 📖	CompOp	1 math math: `adjoin_mem_finset`
`subalgebra` 📖	CompOp	3 math math: `adjoin_mem_finset`, `isLocalization`, `Algebra.instFiniteTypeSubtypeMemSubalgebraSubalgebra`
`submonoid` 📖	CompOp	1 math math: `isLocalization`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_mem_finset` 📖	mathematical	—	`Algebra.adjoin` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `subalgebra` `Subalgebra.toSemiring` `Subalgebra.algebra` `setOf` `Finset` `Finset.instMembership` `finset` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`Algebra.adjoin_adjoin_coe_preimage`
`algHom_ext` 📖	—	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	—	—	`IsLocalization.ringHom_ext` `isLocalization` `IsScalarTower.subalgebra'` `IsScalarTower.right` `AlgHom.ext_of_adjoin_eq_top` `adjoin_mem_finset` `RingHom.ext` `AlgHom.congr_fun` `AlgHom.ext` `RingHom.congr_fun`
`aux` 📖	mathematical	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.adjoin`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `Subalgebra.map` `IsScalarTower.toAlgHom` `Algebra.toSMul`	—	`Algebra.adjoin_induction` `Subalgebra.one_mem` `isUnit_one` `Algebra.mem_sup_right` `Algebra.subset_adjoin` `one_smul` `Algebra.mem_sup_left` `Algebra.smul_def` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_comm` `Subalgebra.mul_mem` `IsUnit.mul` `smul_add` `SemigroupAction.mul_smul` `SMulCommClass.smul_comm` `smulCommClass_self` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `smul_eq_mul` `Algebra.to_smulCommClass` `smul_assoc` `IsScalarTower.right`
`baseChange` 📖	mathematical	—	`Algebra.EssFiniteType` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass`	—	`Algebra.to_smulCommClass` `Algebra.essFiniteType_iff` `TensorProduct.induction_on` `OneMemClass.one_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `Subalgebra.instSubsemiringClass` `isUnit_one` `Finset.coe_image` `Set.image_congr` `mul_one` `IsScalarTower.right` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.mem_map` `Algebra.adjoin_adjoin_of_tower` `TensorProduct.isScalarTower_left` `Algebra.subset_adjoin` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `smul_eq_mul` `TensorProduct.smul_tmul'` `Subalgebra.smul_mem` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `IsUnit.mul` `add_mul` `Distrib.rightDistribClass` `mul_assoc` `mul_comm` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass`
`comp` 📖	mathematical	—	`Algebra.EssFiniteType`	—	`Algebra.essFiniteType_iff` `Finset.coe_union` `Finset.coe_image` `Algebra.adjoin_union` `Algebra.adjoin_image` `aux` `Algebra.smul_def` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `Subalgebra.instSubsemiringClass` `Algebra.mem_sup_left` `IsUnit.mul` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `SemigroupAction.mul_smul` `mul_comm` `smul_mul_assoc` `IsScalarTower.right`
`comp_iff` 📖	mathematical	—	`Algebra.EssFiniteType`	—	`of_comp` `comp`
`cond` 📖	mathematical	—	`IsLocalization` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `SetLike.coe` `Finset` `Finset.instSetLike` `Subalgebra.toCommSemiring` `Submonoid.comap` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `Subalgebra.toSemiring` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `algebraMap` `Subalgebra.toAlgebra` `Algebra.id` `IsUnit.submonoid`	—	—
`iff_of_algEquiv` 📖	mathematical	—	`Algebra.EssFiniteType`	—	`of_surjective` `AlgEquiv.surjective`
`isLocalization` 📖	mathematical	—	`IsLocalization` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `subalgebra` `Subalgebra.toCommSemiring` `submonoid` `Subalgebra.toAlgebra` `Algebra.id`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `cond`
`of_comp` 📖	mathematical	—	`Algebra.EssFiniteType`	—	`Algebra.essFiniteType_iff` `Algebra.adjoin_adjoin_of_tower` `Algebra.subset_adjoin`
`of_finiteType` 📖	mathematical	—	`Algebra.EssFiniteType`	—	`Algebra.essFiniteType_iff` `isUnit_one`
`of_id` 📖	mathematical	—	`Algebra.EssFiniteType` `Algebra.id` `CommRing.toCommSemiring`	—	`of_finiteType` `Module.Finite.finiteType` `Module.Finite.self`
`of_isLocalization` 📖	mathematical	—	`Algebra.EssFiniteType`	—	`Algebra.essFiniteType_iff` `Finset.coe_empty` `Algebra.adjoin_empty` `IsLocalization.surj` `IsLocalization.map_units`
`of_surjective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	`Algebra.EssFiniteType`	—	`IsScalarTower.of_algebraMap_eq'` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap` `Module.Finite.of_surjective` `RingHomSurjective.ids` `Module.Finite.self` `comp` `of_finiteType` `Module.Finite.finiteType`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`essFiniteType_algebraMap` 📖	mathematical	—	`EssFiniteType` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.EssFiniteType`	—	`EssFiniteType.eq_1` `toAlgebra_algebraMap`

RingHom.EssFiniteType

Definitions

Name	Category	Theorems
`finset` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	—	`RingHom.ext` `DFunLike.congr_fun` `Algebra.EssFiniteType.algHom_ext`

RingHom.FiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`essFiniteType` 📖	mathematical	—	`RingHom.EssFiniteType`	—	`Algebra.EssFiniteType.of_finiteType`

---

← Back to Index