Documentation Verification Report

FG

📁 Source: Mathlib/RingTheory/Adjoin/FG.lean

Statistics

Metric	Count
Definitions `FG`, `FG`, `FG`, `FG`, `FG`, `FG`, `FG`, `FG`, `FG`, `FG`, `FG`, `FG`, `FG`, `FG`, `FG`, `FG`, `FG`, `FG`	18
Theorems `isNoetherianRing_range`, `fg_trans`, `FG`, `map`, `prod`, `sup`, `fg_adjoin_finset`, `fg_bot`, `fg_def`, `fg_of_fg_map`, `fg_of_fg_toSubmodule`, `fg_of_noetherian`, `fg_of_submodule_fg`, `fg_top`, `induction_on_adjoin`, `FG`, `isNoetherianRing_of_fg`, `is_noetherian_subring_closure`	18
Total	36

AddGroup

Definitions

Name	Category	Theorems
`FG` 📖	CompData	26 math math: `closure_finite_fg`, `fg_of_surjective`, `AddCommGroup.fg_of_descent'`, `fg_iff_exists_freeAddGroup_hom_surjective_finite`, `fg_iff'`, `Prod.instAddGroupFG`, `fg_iff`, `fg_iff_mul_fg`, `QuotientAddGroup.fg`, `GroupFG.iff_add_fg`, `AddMonoidAlgebra.finiteType_iff_group_fg`, `fg_def`, `fg_iff_addMonoid_fg`, `fg_iff_addSubgroup_fg`, `fg_of_descent`, `fg_of_finite`, `fg_iff_exists_freeAddGroup_hom_surjective`, `instFGInt`, `closure_finset_fg`, `fg_range`, `Module.Finite.iff_addGroup_fg`, `AddCommGroup.fg_of_descent`, `fg_of_group_fg`, `Pi.instAddGroupFG`, `instFGFreeAddGroupOfFinite`, `NumberField.RingOfIntegers.instFG`

AddMonoid

Definitions

Name	Category	Theorems
`FG` 📖	CompData	29 math math: `closure_finite_fg`, `fg_iff`, `instFGFreeAddMonoidOfFinite`, `FreeAbelianGroup.instFG`, `Algebra.GrothendieckAddGroup.instFG`, `AddLocalization.fg`, `closure_finset_fg`, `fg_of_monoid_fg`, `fg_of_finite`, `fG_iff`, `AddGroup.fg_iff_addMonoid_fg`, `fg_iff_exists_freeAddMonoid_hom_surjective`, `Monoid.fg_iff_add_fg`, `fg_range`, `multiples_fg`, `fg_def`, `fg_of_addGroup_fg`, `IsAffineAddMonoid.toFG`, `AddMonoidAlgebra.fg_of_finiteType`, `fg_iff_addSubmonoid_fg`, `AddMonoidAlgebra.finiteType_iff_fg`, `instFGNat`, `AddCommMonoid.fg_of_wellQuasiOrderedLE`, `Module.Finite.iff_addMonoid_fg`, `fg_of_surjective`, `fg_iff_exists_freeAddGroup_hom_surjective_finite`, `Prod.instAddMonoidFG`, `Pi.instAddMonoidFG`, `fg_iff_mul_fg`

AddSemigroupIdeal

Definitions

Name	Category	Theorems
`FG` 📖	MathDef	2 math math: `fg_of_wellQuasiOrderedLE`, `fg_iff`

AddSubgroup

Definitions

Name	Category	Theorems
`FG` 📖	MathDef	18 math math: `Submodule.fg_toAddSubgroup`, `FG.prod`, `fg_iff_addSubmonoid_fg`, `Subgroup.fg_iff_add_fg`, `fg_iff`, `AddGroup.FG.out`, `AddGroup.fg_def`, `Submodule.fg_iff_addSubgroup_fg`, `AddGroup.fg_iff_addSubgroup_fg`, `FG.iSup`, `FG.finset_sup`, `FG.pi`, `FG.biSup_finset`, `FG.biSup`, `fg_iff_mul_fg`, `FG.bot`, `FG.sup`, `fg_iff_exists_fin_addMonoidHom`

AddSubmonoid

Definitions

Name	Category	Theorems
`FG` 📖	MathDef	28 math math: `Submonoid.fg_iff_add_fg`, `FG.pi`, `IsLinearSet.exists_fg_eq_subtypeVal`, `FG.map_injective`, `IsSemilinearSet.exists_fg_eq_subtypeVal`, `AddSubgroup.fg_iff_addSubmonoid_fg`, `FG.iSup`, `fg_of_subtractive`, `fg_eqLocusM`, `AddMonoid.FG.fg_top`, `fg_iff`, `fg_iff_exists_fin_addMonoidHom`, `IsSemilinearSet.exists_fg_eq_subtypeVal₂`, `AddMonoid.fG_iff`, `FG.map`, `FG.bot`, `multiples_fg`, `FG.biSup`, `AddMonoid.fg_def`, `Submodule.fg_iff_addSubmonoid_fg`, `isLinearSet_iff_exists_fg_eq_vadd`, `Nat.addSubmonoid_fg`, `FG.biSup_finset`, `AddMonoid.fg_iff_addSubmonoid_fg`, `FG.prod`, `FG.finset_sup`, `FG.sup`, `fg_iff_mul_fg`

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNoetherianRing_range` 📖	mathematical	—	`IsNoetherianRing` `Subalgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `range` `Subalgebra.toSemiring`	—	`isNoetherianRing_range`

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_trans` 📖	mathematical	`Submodule.FG` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toModule` `DFunLike.coe` `OrderEmbedding` `Subalgebra` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `Subalgebra.toSubmodule` `adjoin` `SetLike.instMembership` `Subalgebra.instSetLike` `Subalgebra.toCommSemiring` `Subalgebra.toAlgebra` `id`	`Submodule.FG` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toModule` `DFunLike.coe` `OrderEmbedding` `Subalgebra` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `Subalgebra.toSubmodule` `adjoin` `Set` `Set.instUnion`	—	`Submodule.fg_def` `Set.Finite.mul` `le_antisymm` `Submodule.span_le` `Set.mul_subset_iff` `Subalgebra.mul_mem` `Submodule.subset_span` `adjoin_mono` `Set.subset_union_left` `IsScalarTower.subalgebra'` `IsScalarTower.right` `adjoin_union_eq_adjoin_adjoin` `Finsupp.mem_span_image_iff_linearCombination` `Set.image_id` `Finsupp.linearCombination_apply` `Finsupp.sum.eq_1` `sum_mem` `Submodule.addSubmonoidClass` `Finsupp.sum_mul` `smul_mul_assoc` `Submodule.smul_mem`

FirstOrder.Language.IsFraisse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`FG` 📖	mathematical	`CategoryTheory.Bundled` `FirstOrder.Language.Structure` `Set` `Set.instMembership`	`FirstOrder.Language.Structure.FG` `CategoryTheory.Bundled.α` `FirstOrder.Language.Structure` `CategoryTheory.Bundled.structure`	—	—

FirstOrder.Language.Structure

Definitions

Name	Category	Theorems
`FG` 📖	CompData	9 math math: `FirstOrder.Language.Equiv.fg_iff`, `fg_def`, `fg_iff_finite`, `FirstOrder.Language.Substructure.fg_iff_structure_fg`, `FG.map_of_surjective`, `FirstOrder.Language.exists_countable_is_age_of_iff`, `FirstOrder.Language.IsFraisse.FG`, `FG.of_finite`, `fg_iff`

FirstOrder.Language.Substructure

Definitions

Name	Category	Theorems
`FG` 📖	MathDef	23 math math: `FirstOrder.Language.IsExtensionPair.cod`, `FirstOrder.Language.Structure.fg_def`, `fg_closure_singleton`, `FirstOrder.Language.PartialEquiv.dom_fg_iff_cod_fg`, `fg_closure`, `FirstOrder.Language.embedding_from_cg`, `fg_iff_structure_fg`, `fg_def`, `FirstOrder.Language.isExtensionPair_iff_cod`, `fg_iff_exists_fin_generating_family`, `FG.sup`, `FirstOrder.Language.equiv_between_cg`, `FirstOrder.Language.age.has_representative_as_substructure`, `instCountable_fg_substructures_of_countable`, `FirstOrder.Language.Structure.FG.range`, `FirstOrder.Language.FGEquiv.symm_coe`, `FG.of_finite`, `FG.of_map_embedding`, `FirstOrder.Language.Structure.FG.out`, `FG.map`, `fg_bot`, `countable_fg_substructures_of_countable`, `fg_iff_finite`

Group

Definitions

Name	Category	Theorems
`FG` 📖	CompData	26 math math: `fg_def`, `Pi.instGroupFG`, `AddGroup.fg_iff_mul_fg`, `fg_of_surjective`, `fg_of_descent`, `Subgroup.fg_of_index_ne_zero`, `fg_iff`, `GroupFG.iff_add_fg`, `CommGroup.fg_of_descent`, `fg_of_mul_group_fg`, `MonoidAlgebra.finiteType_iff_group_fg`, `QuotientGroup.fg`, `fg_iff_exists_freeGroup_hom_surjective_finite`, `Subgroup.instFGSubtypeMemCommutator`, `fg_iff_monoid_fg`, `fg_iff_subgroup_fg`, `instFGFreeGroupOfFinite`, `fg_iff'`, `Prod.instGroupFG`, `closure_finset_fg`, `fg_of_finite`, `CommGroup.fg_of_descent'`, `fg_iff_exists_freeGroup_hom_surjective`, `closureCommutatorRepresentatives_fg`, `fg_range`, `closure_finite_fg`

Ideal

Definitions

Name	Category	Theorems
`FG` 📖	MathDef	27 math math: `fg_of_isNoetherianRing`, `FG.of_FG_map_of_faithfullyFlat`, `FractionalIdeal.coeIdeal_fg`, `FG.pow`, `KaehlerDifferential.ideal_fg`, `FG.map`, `fg_of_localizationSpan`, `FG.mul`, `isNoetherianRing_iff_ideal_fg`, `Algebra.FinitePresentation.ker_fg_of_mvPolynomial`, `RingHom.ker_fg_of_localizationSpan`, `isOka_fg`, `Algebra.FinitePresentation.ker_fG_of_surjective`, `Algebra.FinitePresentation.iff`, `fg_top`, `Algebra.Presentation.fg_ker`, `Polynomial.contentIdeal_FG`, `fg_of_isUnit`, `fg_ker_comp`, `PowerSeries.fg_iff_of_isPrime`, `FG.of_isNoetherianRing`, `Algebra.Generators.fg_ker_of_finitePresentation`, `Algebra.FinitePresentation.out`, `IsSemiprimaryRing.isNoetherianRing_iff_jacobson_fg`, `PrimeSpectrum.isCompact_isOpen_iff_ideal`, `Algebra.FinitePresentation.iff_quotient_mvPolynomial'`, `MvPolynomial.idealOfVars_fg`

IntermediateField

Definitions

Name	Category	Theorems
`FG` 📖	MathDef	12 math math: `fg_adjoin_finset`, `fg_sup`, `fg_def`, `fg_bot`, `FG.of_restrictScalars`, `fg_of_noetherian`, `fg_adjoin_of_finite`, `fg_iSup`, `fg_of_fg_toSubalgebra`, `fg_top`, `fg_top_iff`, `essFiniteType_iff`

Monoid

Definitions

Name	Category	Theorems
`FG` 📖	CompData	26 math math: `CommMonoid.fg_of_wellQuasiOrderedLE`, `Algebra.GrothendieckGroup.instFG`, `IsAffineMonoid.toFG`, `fg_iff_submonoid_fg`, `fg_iff_exists_freeMonoid_hom_surjective`, `fg_range`, `Pi.instMonoidFG`, `MonoidAlgebra.finiteType_iff_fg`, `fg_iff_add_fg`, `instFGFreeMonoidOfFinite`, `closure_finset_fg`, `Localization.fg`, `fg_iff`, `Group.fg_iff_monoid_fg`, `MonoidAlgebra.fg_of_finiteType`, `powers_fg`, `NumberField.Units.instFGUnitsRingOfIntegers`, `fg_iff_exists_freeGroup_hom_surjective_finite`, `fg_of_surjective`, `Prod.instMonoidFG`, `closure_finite_fg`, `fg_of_group_fg`, `fg_of_addMonoid_fg`, `fg_def`, `fg_of_finite`, `AddMonoid.fg_iff_mul_fg`

SemigroupIdeal

Definitions

Name	Category	Theorems
`FG` 📖	MathDef	2 math math: `fg_of_wellQuasiOrderedLE`, `fg_iff`

SubAddAction

Definitions

Name	Category	Theorems
`FG` 📖	MathDef	1 math math: `fg_iff`

SubMulAction

Definitions

Name	Category	Theorems
`FG` 📖	MathDef	1 math math: `fg_iff`

Subalgebra

Definitions

Name	Category	Theorems
`FG` 📖	MathDef	25 math math: `exists_fg_and_mem_baseChange`, `fg_of_fg_toSubmodule`, `fg_of_fg_map`, `fg_of_noetherian`, `TensorProduct.Algebra.eq_of_fg_of_subtype_eq`, `TensorProduct.Algebra.exists_of_fg`, `fg_adjoin_finset`, `FG.prod`, `fg_of_submodule_fg`, `FG.map`, `fg_def`, `fg_iff_finiteType`, `TensorProduct.Algebra.eq_of_fg_of_subtype_eq'`, `exists_subalgebra_of_fg`, `Algebra.fg_trans'`, `reesAlgebra.fg`, `Algebra.Etale.exists_subalgebra_fg`, `FG.sup`, `Submodule.exists_fg_of_baseChange_eq_zero`, `fg_bot`, `fg_top`, `Algebra.FiniteType.out`, `fg_of_fg_of_fg`, `Algebra.Smooth.exists_subalgebra_fg`, `Algebra.IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_adjoin_finset` 📖	mathematical	—	`FG` `Algebra.adjoin` `SetLike.coe` `Finset` `Finset.instSetLike`	—	—
`fg_bot` 📖	mathematical	—	`FG` `Bot.bot` `Subalgebra` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`Algebra.adjoin_empty` `Finset.coe_empty`
`fg_def` 📖	mathematical	—	`FG` `Set` `Set.Finite` `Algebra.adjoin`	—	`Set.exists_finite_iff_finset`
`fg_of_fg_map` 📖	mathematical	`DFunLike.coe` `AlgHom` `AlgHom.funLike` `FG` `map`	`FG`	—	`map_injective` `Algebra.adjoin_image` `Finset.coe_preimage` `Set.image_preimage_eq_of_subset` `AlgHom.coe_range` `Algebra.adjoin_le_iff` `Algebra.map_top` `map_mono` `le_top`
`fg_of_fg_toSubmodule` 📖	mathematical	`Submodule.FG` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `DFunLike.coe` `OrderEmbedding` `Subalgebra` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `toSubmodule`	`FG`	—	`le_antisymm` `Algebra.adjoin_le` `Submodule.subset_span` `Submodule.span_le` `Algebra.subset_adjoin`
`fg_of_noetherian` 📖	mathematical	—	`FG`	—	`fg_of_fg_toSubmodule` `IsNoetherian.noetherian`
`fg_of_submodule_fg` 📖	mathematical	`Submodule.FG` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Top.top` `Submodule` `Submodule.instTop`	`FG` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`RelEmbedding.injective` `Algebra.top_toSubmodule` `eq_top_iff` `Submodule.span_le` `Algebra.subset_adjoin`
`fg_top` 📖	mathematical	—	`FG` `Subalgebra` `SetLike.instMembership` `instSetLike` `toSemiring` `algebra` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`range_val` `Algebra.map_top` `FG.map` `fg_of_fg_map` `Subtype.val_injective`
`induction_on_adjoin` 📖	—	`Bot.bot` `Subalgebra` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Algebra.adjoin` `Set` `Set.instInsert` `SetLike.coe` `instSetLike`	—	—	`fg_of_noetherian` `Finset.induction_on` `Finset.coe_empty` `Algebra.adjoin_empty` `Finset.coe_insert` `Algebra.adjoin_insert_adjoin`

Subalgebra.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map` 📖	mathematical	`Subalgebra.FG`	`Subalgebra.FG` `Subalgebra.map`	—	`Finset.coe_image` `Algebra.adjoin_image`
`prod` 📖	mathematical	`Subalgebra.FG`	`Subalgebra.FG` `Prod.instSemiring` `Prod.algebra` `Subalgebra.prod`	—	`Subalgebra.fg_def` `Set.Finite.union` `Set.Finite.image` `Set.finite_singleton` `Algebra.adjoin_inl_union_inr_eq_prod`
`sup` 📖	mathematical	`Subalgebra.FG`	`Subalgebra.FG` `Subalgebra` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra`	—	`Subalgebra.fg_def` `Set.Finite.union` `Algebra.adjoin_union`

Subgroup

Definitions

Name	Category	Theorems
`FG` 📖	MathDef	15 math math: `Group.fg_def`, `FG.biSup`, `fg_iff_submonoid_fg`, `FG.finset_sup`, `fg_iff_add_fg`, `fg_iff`, `FG.biSup_finset`, `FG.pi`, `FG.sup`, `Group.fg_iff_subgroup_fg`, `FG.iSup`, `AddSubgroup.fg_iff_mul_fg`, `FG.prod`, `Group.FG.out`, `FG.bot`

Submodule

Definitions

Name	Category	Theorems
`FG` 📖	MathDef	104 math math: `Module.FinitePresentation.fg_ker`, `FG.rTensor.directedSystem`, `fg_iff_spanRank_eq_spanFinrank`, `fg_of_isUnit`, `FractionalIdeal.fg_of_isUnit`, `TensorProduct.eq_of_fg_of_subtype_eq'`, `isNoetherian_submodule_right`, `fg_pi`, `exists_fg_le_eq_rTensor_inclusion`, `Module.Finite.fg_top`, `FG.restrictScalars_of_surjective`, `FractionalIdeal.fg_unit`, `FractionalIdeal.coeIdeal_fg`, `fg_of_ker_bot`, `fg_map_iff`, `FG.lTensor.directedSystem`, `FG.exists_rTensor_fg_inclusion_eq`, `FG.prod`, `isNoetherian_submodule`, `fg_biSup`, `PointedCone.DualFG.exists_fg_dual`, `FG.restrictScalars`, `Module.FinitePresentation.equiv_quotient`, `Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective`, `IsPrincipal.fg`, `range_fg_iff_ker_cofg`, `fg_def`, `ZLattice.FG`, `FG.map`, `fg_iff_exists_finite_generating_family`, `FG.restrictScalars_iff`, `spanRank_finite_iff_fg`, `Module.FinitePresentation.exists_fin`, `isNoetherian_iff_fg_wellFounded`, `fg_span_iff_fg_span_finset_subset`, `fg_restrictScalars`, `FG.lTensor.directLimit_apply'`, `FG.rTensor.directLimit_apply`, `FractionalIdeal.fg_of_isNoetherianRing`, `fg_range`, `mem_integralClosure_iff_mem_fg`, `exists_fg_le_subset_range_rTensor_subtype`, `IsNoetherian.noetherian`, `Algebra.fg_trans`, `fg_iSup`, `fg_finset_sup`, `fg_iff_addSubgroup_fg`, `TensorProduct.eq_zero_of_fg_of_subtype_eq_zero`, `FG.pow`, `Ideal.is_fg_degreeLE`, `exists_subalgebra_of_fg`, `isNoetherian_def`, `fg_of_linearEquiv`, `Module.finite_def`, `fg_iff_addSubmonoid_fg`, `FG.mul`, `fg_adjoin_of_finite`, `fg_iff_exists_fin_generating_family`, `fg_of_injective`, `FractionalIdeal.isNoetherian_iff`, `fg_of_isLocalized_maximal`, `Module.fgSystem.instIsDirectedOrderSubtypeSubmoduleFG`, `TensorProduct.eq_of_fg_of_subtype_eq`, `Module.FinitePresentation.out`, `FG.directedSystem`, `fg_iff_exists_fin_linearMap`, `IsLattice.fg`, `FG.lTensor.directLimit_apply`, `FG.map₂`, `Module.fgSystem.equiv_comp_of`, `Module.Finite.iff_fg`, `fg_top`, `fg_iff_finiteDimensional`, `fg_span_singleton`, `exists_fg_le_subset_range_rTensor_inclusion`, `fg_iff_compact`, `FG.of_le_of_isNoetherian`, `FG.span`, `FG.of_le`, `isNoetherian_submodule_left`, `exists_fg_le_eq_rTensor_subtype`, `IsIntegral.fg_adjoin_singleton`, `Module.FinitePresentation.fg_ker_iff`, `FG.sup`, `fg_bot`, `FG.of_finite`, `fg_of_fg_map`, `Module.fgSystem.instDirectedSystemSubtypeSubmoduleFGMemValCoeLinearMapId`, `fg_ker_comp`, `IsLocalization.coeSubmodule_fg`, `FG.smul`, `fg_span`, `fg_of_localized_maximal`, `FG.rTensor.directLimit_apply'`, `CoFG.fg_of_isCompl`, `fg_of_fg_map_injective`, `FG.of_restrictScalars`, `fg_of_fg_map_of_fg_inf_ker`, `TensorProduct.exists_of_fg`, `PointedCone.DualFG.iff_exists_fg_dual`, `Subalgebra.fg_bot_toSubmodule`, `Ideal.Filtration.submodule_fg_iff_stable`, `fg_unit`, `Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective`

Submonoid

Definitions

Name	Category	Theorems
`FG` 📖	MathDef	20 math math: `fg_iff_add_fg`, `Monoid.fg_iff_submonoid_fg`, `fg_of_divisive`, `fg_eqLocusM`, `Monoid.FG.fg_top`, `Subgroup.fg_iff_submonoid_fg`, `FG.finset_sup`, `FG.prod`, `powers_fg`, `FG.iSup`, `FG.pi`, `fg_iff`, `FG.sup`, `FG.map`, `FG.map_injective`, `FG.biSup_finset`, `FG.bot`, `AddSubmonoid.fg_iff_mul_fg`, `Monoid.fg_def`, `FG.biSup`

ZLattice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`FG` 📖	mathematical	—	`Submodule.FG` `Int.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toIntModule` `NormedAddCommGroup.toAddCommGroup`	—	`exists_linearIndependent` `Submodule.fg_of_fg_map_of_fg_inf_ker` `RingHomSurjective.ids` `Submodule.fg_def` `IsZLattice.span_top` `Submodule.span_mono` `Subtype.range_coe_subtype` `Set.instReflSubset` `LinearIndependent.setFinite` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Set.Finite.of_finite_image` `Metric.finite_isBounded_inter_isClosed` `DiscreteTopology.isDiscrete` `ZSpan.fundamentalDomain_isBounded` `Finite.of_fintype` `AddSubgroup.isClosed_of_discrete` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Set.Finite.subset` `Submodule.mkQ_apply` `ZSpan.fractRestrict_apply` `ZSpan.fract_mem_fundamentalDomain` `ZSpan.fract.eq_1` `SetLike.mem_coe` `sub_eq_add_neg` `Submodule.add_mem` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `Submodule.addSubgroupClass` `Set.mem_of_subset_of_mem` `SetLike.coe_subset_coe` `instIsConcreteLE` `Set.setOf_mem_eq` `Submodule.span_le` `Subtype.mem` `Function.Injective.injOn` `Subtype.coe_injective` `Equiv.injective` `Submodule.span_eq` `Submodule.ker_mkQ` `inf_of_le_right` `Submodule.fg_span`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNoetherianRing_of_fg` 📖	mathematical	`Subalgebra.FG` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	`IsNoetherianRing` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Subalgebra.toSemiring`	—	`AlgHom.isNoetherianRing_range` `MvPolynomial.isNoetherianRing` `Finite.of_fintype` `Algebra.adjoin_eq_range`
`is_noetherian_subring_closure` 📖	mathematical	—	`IsNoetherianRing` `Subring` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `SetLike.instMembership` `Subring.instSetLike` `Subring.closure` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `CommRing.toCommSemiring` `SubringClass.toSubsemiringClass` `Subring.instSubringClass`	—	`isNoetherianRing_of_fg` `Subalgebra.fg_def` `isNoetherian_of_isNoetherianRing_of_finite` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `AddGroup.instFGInt` `Algebra.adjoin_int`

---

← Back to Index