Documentation Verification Report

FiniteType

📁 Source: Mathlib/RingTheory/FiniteType.lean

Statistics

Metric	Count
Definitions	0
Theorems `exists_finset_adjoin_eq_top`, `fg_of_finiteType`, `finiteType_iff_fg`, `finiteType_iff_group_fg`, `finiteType_of_fg`, `freeAlgebra_lift_of_surjective_of_closure`, `mem_adjoin_support`, `mvPolynomial_aeval_of_surjective_of_closure`, `support_gen_of_gen`, `support_gen_of_gen'`, `finiteType`, `comp`, `comp_surjective`, `id`, `of_comp_finiteType`, `of_surjective`, `adjoin_of_finite`, `equiv`, `iff_quotient_freeAlgebra`, `iff_quotient_freeAlgebra'`, `iff_quotient_mvPolynomial`, `iff_quotient_mvPolynomial'`, `iff_quotient_mvPolynomial''`, `instFreeAlgebraOfFinite`, `instMvPolynomialOfFinite`, `instPolynomial`, `isNoetherianRing`, `of_restrictScalars_finiteType`, `of_surjective`, `out`, `prod`, `quotient`, `trans`, `orzechProperty`, `finiteType`, `exists_finset_adjoin_eq_top`, `fg_of_finiteType`, `finiteType_iff_fg`, `finiteType_iff_group_fg`, `finiteType_of_fg`, `freeAlgebra_lift_of_surjective_of_closure`, `mem_adjoin_support`, `mvPolynomial_aeval_of_surjective_of_closure`, `support_gen_of_gen`, `support_gen_of_gen'`, `finiteType`, `to_finiteType`, `comp`, `comp_surjective`, `id`, `of_comp_finiteType`, `of_finite`, `of_surjective`, `finiteType_algebraMap`, `fg_iff_finiteType`	55
Total	55

AddMonoidAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_finset_adjoin_eq_top` 📖	mathematical	—	`Algebra.adjoin` `AddMonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semiring` `algebra` `Algebra.id` `Set.image` `of'` `SetLike.coe` `Finset` `Finset.instSetLike` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`Finset.coe_biUnion` `support_gen_of_gen'`
`fg_of_finiteType` 📖	mathematical	—	`AddMonoid.FG`	—	`finiteType_iff_fg`
`finiteType_iff_fg` 📖	mathematical	—	`Algebra.FiniteType` `AddMonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semiring` `algebra` `Algebra.id` `AddMonoid.FG`	—	`exists_finset_adjoin_eq_top` `AddMonoid.fg_def` `AddSubmonoid.eq_top_iff'` `mem_closure_of_mem_span_closure` `Algebra.adjoin_eq_span` `finiteType_of_fg`
`finiteType_iff_group_fg` 📖	mathematical	—	`Algebra.FiniteType` `AddMonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `algebra` `Algebra.id` `AddGroup.FG`	—	`finiteType_iff_fg`
`finiteType_of_fg` 📖	mathematical	—	`Algebra.FiniteType` `AddMonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semiring` `algebra` `Algebra.id`	—	`AddMonoid.FG.fg_top` `Algebra.FiniteType.of_surjective` `Algebra.FiniteType.instFreeAlgebraOfFinite` `Finite.of_fintype` `Module.Finite.finiteType` `Module.Finite.self` `freeAlgebra_lift_of_surjective_of_closure`
`freeAlgebra_lift_of_surjective_of_closure` 📖	mathematical	`AddSubmonoid.closure` `AddMonoid.toAddZeroClass` `Top.top` `AddSubmonoid` `AddSubmonoid.instTop`	`FreeAlgebra` `Set.Elem` `AddMonoidAlgebra` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `FreeAlgebra.instSemiring` `semiring` `FreeAlgebra.instAlgebra` `Algebra.id` `algebra` `AlgHom.funLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeAlgebra.lift` `of'` `Set` `Set.instMembership`	—	`induction_on` `AddSubmonoid.mem_top` `AddSubmonoid.closure_induction` `FreeAlgebra.lift_ι_apply` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `of_apply` `single_mul_single` `one_mul` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass`
`mem_adjoin_support` 📖	mathematical	—	`AddMonoidAlgebra` `CommSemiring.toSemiring` `Subalgebra` `semiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.image` `of'` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Submodule.span_le` `Algebra.subset_adjoin` `mem_span_support`
`mvPolynomial_aeval_of_surjective_of_closure` 📖	mathematical	`AddSubmonoid.closure` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Top.top` `AddSubmonoid` `AddSubmonoid.instTop`	`MvPolynomial` `Set.Elem` `AddMonoidAlgebra` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `MvPolynomial.commSemiring` `commSemiring` `MvPolynomial.algebra` `Algebra.id` `algebra` `AlgHom.funLike` `MvPolynomial.aeval` `of'` `Set` `Set.instMembership`	—	`induction_on` `AddSubmonoid.mem_top` `AddSubmonoid.closure_induction` `MvPolynomial.aeval_X` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `of_apply` `single_mul_single` `one_mul` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass`
`support_gen_of_gen` 📖	mathematical	`Algebra.adjoin` `AddMonoidAlgebra` `CommSemiring.toSemiring` `semiring` `algebra` `Algebra.id` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`Set.iUnion` `Set` `Set.instMembership` `Set.image` `of'` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`le_antisymm` `le_top` `Algebra.adjoin_le_iff` `Set.mem_iUnion₂` `Algebra.adjoin_mono` `mem_adjoin_support`
`support_gen_of_gen'` 📖	mathematical	`Algebra.adjoin` `AddMonoidAlgebra` `CommSemiring.toSemiring` `semiring` `algebra` `Algebra.id` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`Set.image` `of'` `Set.iUnion` `Set` `Set.instMembership` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Set.image_iUnion` `support_gen_of_gen`

AlgHom.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finiteType` 📖	mathematical	—	`AlgHom.FiniteType`	—	`RingHom.Finite.finiteType`

AlgHom.FiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`AlgHom.FiniteType` `AlgHom.comp` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`RingHom.FiniteType.comp`
`comp_surjective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	`AlgHom.FiniteType` `AlgHom.comp`	—	`RingHom.FiniteType.comp_surjective`
`id` 📖	mathematical	—	`AlgHom.FiniteType` `AlgHom.id` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`RingHom.FiniteType.id`
`of_comp_finiteType` 📖	mathematical	—	`AlgHom.FiniteType`	—	`RingHom.FiniteType.of_comp_finiteType`
`of_surjective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	`AlgHom.FiniteType`	—	`RingHom.FiniteType.of_surjective`

Algebra.FiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_of_finite` 📖	mathematical	—	`Algebra.FiniteType` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Subalgebra.toSemiring` `Subalgebra.algebra`	—	`Subalgebra.fg_iff_finiteType` `Set.Finite.coe_toFinset`
`equiv` 📖	mathematical	—	`Algebra.FiniteType`	—	`of_surjective` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AlgEquiv.surjective`
`iff_quotient_freeAlgebra` 📖	mathematical	—	`Algebra.FiniteType` `FreeAlgebra` `Finset` `SetLike.instMembership` `Finset.instSetLike` `DFunLike.coe` `AlgHom` `FreeAlgebra.instSemiring` `FreeAlgebra.instAlgebra` `Algebra.id` `AlgHom.funLike`	—	`Set.range_eq_univ` `AlgHom.coe_range` `Algebra.adjoin_range_eq_range_freeAlgebra_lift` `Subtype.range_coe_subtype` `Finset.setOf_mem` `Algebra.coe_top` `of_surjective` `instFreeAlgebraOfFinite` `Finite.of_fintype` `Module.Finite.finiteType` `Module.Finite.self`
`iff_quotient_freeAlgebra'` 📖	mathematical	—	`Algebra.FiniteType` `FreeAlgebra` `DFunLike.coe` `AlgHom` `FreeAlgebra.instSemiring` `FreeAlgebra.instAlgebra` `Algebra.id` `AlgHom.funLike`	—	`iff_quotient_freeAlgebra` `of_surjective` `instFreeAlgebraOfFinite` `Finite.of_fintype` `Module.Finite.finiteType` `Module.Finite.self`
`iff_quotient_mvPolynomial` 📖	mathematical	—	`Algebra.FiniteType` `CommSemiring.toSemiring` `MvPolynomial` `Finset` `Finset.instMembership` `DFunLike.coe` `AlgHom` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike`	—	`Set.mem_range` `AlgHom.coe_range` `Algebra.adjoin_eq_range` `Set.mem_univ` `of_surjective` `instMvPolynomialOfFinite` `Finite.of_fintype` `Module.Finite.finiteType` `Module.Finite.self`
`iff_quotient_mvPolynomial'` 📖	mathematical	—	`Algebra.FiniteType` `CommSemiring.toSemiring` `MvPolynomial` `DFunLike.coe` `AlgHom` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike`	—	`iff_quotient_mvPolynomial` `of_surjective` `instMvPolynomialOfFinite` `Finite.of_fintype` `Module.Finite.finiteType` `Module.Finite.self`
`iff_quotient_mvPolynomial''` 📖	mathematical	—	`Algebra.FiniteType` `CommSemiring.toSemiring` `MvPolynomial` `DFunLike.coe` `AlgHom` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike`	—	`iff_quotient_mvPolynomial'` `of_surjective` `instMvPolynomialOfFinite` `Finite.of_fintype` `Module.Finite.finiteType` `Module.Finite.self`
`instFreeAlgebraOfFinite` 📖	mathematical	—	`Algebra.FiniteType` `FreeAlgebra` `FreeAlgebra.instSemiring` `FreeAlgebra.instAlgebra`	—	`nonempty_fintype` `trans` `FreeAlgebra.instIsScalarTower` `IsScalarTower.right` `Finset.coe_image` `Finset.coe_univ` `Set.image_univ` `FreeAlgebra.adjoin_range_ι`
`instMvPolynomialOfFinite` 📖	mathematical	—	`Algebra.FiniteType` `MvPolynomial` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra`	—	`nonempty_fintype` `trans` `MvPolynomial.isScalarTower` `IsScalarTower.right` `Finset.coe_image` `Finset.coe_univ` `Set.image_univ` `MvPolynomial.adjoin_range_X`
`instPolynomial` 📖	mathematical	—	`Algebra.FiniteType` `Polynomial` `CommSemiring.toSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra`	—	`trans` `Polynomial.isScalarTower` `IsScalarTower.right` `Finset.coe_singleton` `Polynomial.adjoin_X`
`isNoetherianRing` 📖	mathematical	—	`IsNoetherianRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`out` `isNoetherianRing_of_surjective` `Set.range_eq_univ` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.toRingHom_eq_coe` `RingHom.coe_coe` `AlgHom.coe_range` `Algebra.adjoin_range_eq_range_aeval` `Subtype.range_coe_subtype` `Finset.setOf_mem` `MvPolynomial.isNoetherianRing` `Finite.of_fintype`
`of_restrictScalars_finiteType` 📖	mathematical	—	`Algebra.FiniteType`	—	`out` `Algebra.eq_top_iff` `Algebra.adjoin_le` `Algebra.subset_adjoin`
`of_surjective` 📖	mathematical	`DFunLike.coe` `AlgHom` `AlgHom.funLike`	`Algebra.FiniteType`	—	`Algebra.map_top` `Subalgebra.FG.map` `out`
`out` 📖	mathematical	—	`Subalgebra.FG` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	—
`prod` 📖	mathematical	—	`Algebra.FiniteType` `Prod.instSemiring` `Prod.algebra`	—	`Subalgebra.prod_top` `Subalgebra.FG.prod` `out`
`quotient` 📖	mathematical	—	`Algebra.FiniteType` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient`	—	`trans` `Ideal.Quotient.isScalarTower` `IsScalarTower.right` `Module.Finite.finiteType` `Module.Finite.quotient` `Module.Finite.self`
`trans` 📖	mathematical	—	`Algebra.FiniteType`	—	`Algebra.fg_trans'` `out`

CommRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orzechProperty` 📖	mathematical	—	`OrzechProperty` `CommSemiring.toSemiring` `toCommSemiring`	—	`Submodule.injective_subtype` `LinearMap.ker_eq_bot` `LinearMap.ker_eq_bot'` `Module.Finite.exists_fin` `RingHomInvPair.ids` `smulCommClass_self` `Finite.of_fintype` `Module.surjective_piEquiv_apply_iff` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `Submodule.subset_span` `LinearMap.IsScalarTower.compatibleSMul` `Subring.instIsScalarTowerSubtypeMem` `Submodule.isScalarTower'` `IsScalarTower.left` `Submodule.span_induction` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_add` `SemilinearMapClass.toAddHomClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Submodule.smul_mem` `IsNoetherian.injective_of_surjective_of_injective` `isNoetherian_of_isNoetherianRing_of_finite` `is_noetherian_subring_closure` `Set.Finite.union` `Set.finite_range` `Finite.instProd` `Module.Finite.span_of_finite` `Module.piEquiv_apply_apply` `Submodule.sum_mem` `Subring.subset_closure` `RingHomSurjective.ids` `Subtype.val_injective`

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finiteType` 📖	mathematical	—	`Algebra.FiniteType`	—	`Subalgebra.fg_of_submodule_fg` `fg_top`

MonoidAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_finset_adjoin_eq_top` 📖	mathematical	—	`Algebra.adjoin` `MonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semiring` `algebra` `Algebra.id` `Set.image` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of` `SetLike.coe` `Finset` `Finset.instSetLike` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`Finset.coe_biUnion` `support_gen_of_gen'`
`fg_of_finiteType` 📖	mathematical	—	`Monoid.FG`	—	`finiteType_iff_fg`
`finiteType_iff_fg` 📖	mathematical	—	`Algebra.FiniteType` `MonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semiring` `algebra` `Algebra.id` `Monoid.FG`	—	`Monoid.fg_iff_add_fg` `AddMonoidAlgebra.finiteType_iff_fg` `Algebra.FiniteType.equiv` `finiteType_of_fg`
`finiteType_iff_group_fg` 📖	mathematical	—	`Algebra.FiniteType` `MonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `algebra` `Algebra.id` `Group.FG`	—	`finiteType_iff_fg`
`finiteType_of_fg` 📖	mathematical	—	`Algebra.FiniteType` `MonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semiring` `algebra` `Algebra.id`	—	`Algebra.FiniteType.equiv` `AddMonoidAlgebra.finiteType_of_fg` `AddMonoid.fg_of_monoid_fg`
`freeAlgebra_lift_of_surjective_of_closure` 📖	mathematical	`Submonoid.closure` `Monoid.toMulOneClass` `Top.top` `Submonoid` `Submonoid.instTop`	`FreeAlgebra` `Set.Elem` `MonoidAlgebra` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `FreeAlgebra.instSemiring` `semiring` `FreeAlgebra.instAlgebra` `Algebra.id` `algebra` `AlgHom.funLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeAlgebra.lift` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of` `Set` `Set.instMembership`	—	`induction_on` `Submonoid.mem_top` `Submonoid.closure_induction` `FreeAlgebra.lift_ι_apply` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `of_apply` `single_mul_single` `one_mul` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass`
`mem_adjoin_support` 📖	mathematical	—	`MonoidAlgebra` `CommSemiring.toSemiring` `Subalgebra` `semiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.image` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Submodule.span_le` `Algebra.subset_adjoin` `mem_span_support`
`mvPolynomial_aeval_of_surjective_of_closure` 📖	mathematical	`Submonoid.closure` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Top.top` `Submonoid` `Submonoid.instTop`	`MvPolynomial` `Set.Elem` `MonoidAlgebra` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `MvPolynomial.commSemiring` `commSemiring` `MvPolynomial.algebra` `Algebra.id` `algebra` `AlgHom.funLike` `MvPolynomial.aeval` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of` `Set` `Set.instMembership`	—	`induction_on` `Submonoid.mem_top` `Submonoid.closure_induction` `MvPolynomial.aeval_X` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `of_apply` `single_mul_single` `one_mul` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass`
`support_gen_of_gen` 📖	mathematical	`Algebra.adjoin` `MonoidAlgebra` `CommSemiring.toSemiring` `semiring` `algebra` `Algebra.id` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`Set.iUnion` `Set` `Set.instMembership` `Set.image` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`le_antisymm` `le_top` `Algebra.adjoin_le_iff` `Set.mem_iUnion₂` `Algebra.adjoin_mono` `mem_adjoin_support`
`support_gen_of_gen'` 📖	mathematical	`Algebra.adjoin` `MonoidAlgebra` `CommSemiring.toSemiring` `semiring` `algebra` `Algebra.id` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`Set.image` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of` `Set.iUnion` `Set` `Set.instMembership` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Set.image_iUnion` `support_gen_of_gen`

RingHom

Theorems

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

RingHom.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finiteType` 📖	mathematical	—	`RingHom.FiniteType`	—	`Module.Finite.finiteType`
`to_finiteType` 📖	mathematical	—	`RingHom.FiniteType`	—	`RingHom.FiniteType.of_finite`

RingHom.FiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`RingHom.FiniteType` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`IsScalarTower.of_algebraMap_eq'` `Algebra.FiniteType.trans`
`comp_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	`RingHom.FiniteType` `RingHom.comp`	—	`Algebra.FiniteType.of_surjective` `OneHom.map_one'` `MonoidHom.map_mul'` `RingHom.map_zero'` `RingHom.map_add'`
`id` 📖	mathematical	—	`RingHom.FiniteType` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Module.Finite.finiteType` `Module.Finite.self`
`of_comp_finiteType` 📖	mathematical	—	`RingHom.FiniteType`	—	`IsScalarTower.of_algebraMap_eq'` `Algebra.FiniteType.of_restrictScalars_finiteType`
`of_finite` 📖	mathematical	—	`RingHom.FiniteType`	—	`Module.Finite.finiteType`
`of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	`RingHom.FiniteType`	—	`RingHom.comp_id` `comp_surjective` `id`

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_iff_finiteType` 📖	mathematical	—	`FG` `Algebra.FiniteType` `Subalgebra` `SetLike.instMembership` `instSetLike` `toSemiring` `algebra`	—	`fg_top` `Algebra.FiniteType.out`

---

← Back to Index