Commit 2023-03-18 17:27 e5ec18f3

View on Github →

feat: port RingTheory.Finiteness (#2811)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/RestrictScalars.lean

Created Mathlib/RingTheory/Finiteness.lean

added theorem AlgHom.Finite.comp

added theorem AlgHom.Finite.id

added theorem AlgHom.Finite.of_comp_finite

added theorem AlgHom.Finite.of_surjective

added def AlgHom.Finite

added theorem Ideal.Fg.map

added def Ideal.Fg

added theorem Ideal.exists_radical_pow_le_of_fg

added theorem Ideal.fg_ker_comp

added theorem Module.Finite.equiv

added theorem Module.Finite.exists_fin

added theorem Module.Finite.iff_addGroup_fg

added theorem Module.Finite.iff_addMonoid_fg

added theorem Module.Finite.of_restrictScalars_finite

added theorem Module.Finite.of_surjective

added theorem Module.Finite.trans

added theorem Module.finite_def

added theorem RingHom.Finite.comp

added theorem RingHom.Finite.id

added theorem RingHom.Finite.of_comp_finite

added theorem RingHom.Finite.of_surjective

added def RingHom.Finite

added theorem Subalgebra.fg_bot_toSubmodule

added theorem Submodule.Fg.map

added theorem Submodule.Fg.map₂

added theorem Submodule.Fg.mul

added theorem Submodule.Fg.pow

added theorem Submodule.Fg.prod

added theorem Submodule.Fg.stablizes_of_supᵢ_eq

added theorem Submodule.Fg.sup

added def Submodule.Fg

added theorem Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul

added theorem Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul

added theorem Submodule.fg_bot

added theorem Submodule.fg_bsupr

added theorem Submodule.fg_def

added theorem Submodule.fg_finset_sup

added theorem Submodule.fg_iff_addSubmonoid_fg

added theorem Submodule.fg_iff_add_subgroup_fg

added theorem Submodule.fg_iff_compact

added theorem Submodule.fg_iff_exists_fin_generating_family

added theorem Submodule.fg_induction

added theorem Submodule.fg_ker_comp

added theorem Submodule.fg_of_fg_map

added theorem Submodule.fg_of_fg_map_injective

added theorem Submodule.fg_of_fg_map_of_fg_inf_ker

added theorem Submodule.fg_of_isUnit

added theorem Submodule.fg_of_linearEquiv

added theorem Submodule.fg_pi

added theorem Submodule.fg_restrictScalars

added theorem Submodule.fg_span

added theorem Submodule.fg_span_singleton

added theorem Submodule.fg_supᵢ

added theorem Submodule.fg_top

added theorem Submodule.fg_unit