Defs

📁 Source: Mathlib/RingTheory/Finiteness/Defs.lean

Statistics

Metric	Count
Definitions	0
Theorems to_moduleFinite_int, to_moduleFinite_nat, exists_fin, fg_top, iff_addGroup_fg, iff_addMonoid_fg, finite_def, finite_algebraMap, fg_def, fg_iff_addSubgroup_fg, fg_iff_addSubmonoid_fg, fg_iff_add_subgroup_fg, fg_iff_exists_fin_generating_family, fg_iff_exists_finite_generating_family, fg_span_iff_fg_span_finset_subset	15
Total	15

AddMonoid.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_moduleFinite_int 📖	mathematical	—	Module.Finite Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule	—	Module.Finite.iff_addGroup_fg AddGroup.fg_iff_addMonoid_fg
to_moduleFinite_nat 📖	mathematical	—	Module.Finite Nat.instSemiring AddCommMonoid.toNatModule	—	Module.Finite.iff_addMonoid_fg

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_def 📖	mathematical	—	Finite Submodule.FG Top.top Submodule Submodule.instTop	—	Finite.fg_top

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_fin 📖	mathematical	—	Submodule.span Set.range Top.top Submodule Submodule.instTop	—	Submodule.fg_iff_exists_fin_generating_family fg_top
fg_top 📖	mathematical	—	Submodule.FG Top.top Submodule Submodule.instTop	—	—
iff_addGroup_fg 📖	mathematical	—	Module.Finite Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule AddGroup.FG AddCommGroup.toAddGroup	—	AddGroup.fg_def Submodule.fg_iff_addSubgroup_fg fg_top
iff_addMonoid_fg 📖	mathematical	—	Module.Finite Nat.instSemiring AddCommMonoid.toNatModule AddMonoid.FG AddCommMonoid.toAddMonoid	—	AddMonoid.fg_def Submodule.fg_iff_addSubmonoid_fg fg_top

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_algebraMap 📖	mathematical	—	Finite algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Module.Finite NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule	—	Finite.eq_1 toAlgebra_algebraMap

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fg_def 📖	mathematical	—	FG Set.Finite span	—	Finset.finite_toSet Set.Finite.exists_finset_coe
fg_iff_addSubgroup_fg 📖	mathematical	—	FG Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule AddSubgroup.FG AddCommGroup.toAddGroup toAddSubgroup Int.instRing	—	—
fg_iff_addSubmonoid_fg 📖	mathematical	—	FG Nat.instSemiring AddCommMonoid.toNatModule AddSubmonoid.FG AddCommMonoid.toAddMonoid toAddSubmonoid	—	—
fg_iff_add_subgroup_fg 📖	mathematical	—	FG Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule AddSubgroup.FG AddCommGroup.toAddGroup toAddSubgroup Int.instRing	—	fg_iff_addSubgroup_fg
fg_iff_exists_fin_generating_family 📖	mathematical	—	FG span Set.range	—	fg_def Set.Finite.fin_embedding Set.finite_range Finite.of_fintype
fg_iff_exists_finite_generating_family 📖	mathematical	—	FG span Set.range	—	fg_iff_exists_fin_generating_family instFiniteULift Finite.of_fintype Set.ext Finite.Set.finite_range Set.coe_toFinset
fg_span_iff_fg_span_finset_subset 📖	mathematical	—	FG span Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike	—	subset_span_finite_of_subset_span subset_span le_antisymm span_le le_trans

---

← Back to Index