Commit 2026-03-03 14:56 3426e8e0

View on Github →

chore(RingTheory): reorganize imports around locality properties of finiteness (#36044)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Finiteness/FinitePresentationLocal.lean

added theorem Algebra.FinitePresentation.of_span_eq_top_target

added theorem Algebra.FinitePresentation.of_span_eq_top_target_aux

added theorem Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway

Created Mathlib/RingTheory/Finiteness/FiniteTypeLocal.lean

added theorem Algebra.FiniteType.of_span_eq_top_source

added theorem Algebra.FiniteType.of_span_eq_top_target

added theorem IsLocalization.exists_smul_mem_of_mem_adjoin

added theorem IsLocalization.lift_mem_adjoin_finsetIntegerMultiple

Modified Mathlib/RingTheory/Localization/Finiteness.lean

added theorem IsLocalization.smul_mem_finsetIntegerMultiple_span

added theorem Module.Finite.of_isLocalization

added theorem multiple_mem_adjoin_of_mem_localization_adjoin

added theorem multiple_mem_span_of_mem_localization_span

Modified Mathlib/RingTheory/RingHom/Finite.lean

deleted theorem IsLocalization.smul_mem_finsetIntegerMultiple_span

deleted theorem Module.Finite.of_isLocalization

deleted theorem multiple_mem_adjoin_of_mem_localization_adjoin

deleted theorem multiple_mem_span_of_mem_localization_span

Modified Mathlib/RingTheory/RingHom/FinitePresentation.lean

deleted theorem Algebra.FinitePresentation.of_span_eq_top_target

deleted theorem Algebra.FinitePresentation.of_span_eq_top_target_aux

deleted theorem Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway

Modified Mathlib/RingTheory/RingHom/FiniteType.lean

deleted theorem Algebra.FiniteType.of_span_eq_top_source

deleted theorem Algebra.FiniteType.of_span_eq_top_target

deleted theorem IsLocalization.exists_smul_mem_of_mem_adjoin

deleted theorem IsLocalization.lift_mem_adjoin_finsetIntegerMultiple

Modified Mathlib/RingTheory/Support.lean