Commit 2024-12-26 12:12 a0a62fed

View on Github →

feat(Algebra/Colimit/ModuleRing): split into Module and Ring (#20247) 20 files see a 100+ decrease in transitive imports.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/AlgebraCat/Limits.lean

Modified Mathlib/Algebra/Category/ModuleCat/Limits.lean

Modified Mathlib/Algebra/Colimit/DirectLimit.lean

Renamed Mathlib/Algebra/Colimit/ModuleRing.lean to Mathlib/Algebra/Colimit/Module.lean

deleted theorem Field.DirectLimit.exists_inv

deleted def Ring.DirectLimit.congr

deleted theorem Ring.DirectLimit.congr_apply_of

deleted theorem Ring.DirectLimit.congr_symm_apply_of

deleted theorem Ring.DirectLimit.exists_of

deleted theorem Ring.DirectLimit.induction_on

deleted def Ring.DirectLimit.lift

deleted theorem Ring.DirectLimit.lift_injective

deleted theorem Ring.DirectLimit.lift_of

deleted theorem Ring.DirectLimit.lift_unique

deleted def Ring.DirectLimit.map

deleted theorem Ring.DirectLimit.map_apply_of

deleted theorem Ring.DirectLimit.map_comp

deleted theorem Ring.DirectLimit.map_id

deleted theorem Ring.DirectLimit.of.zero_exact

deleted theorem Ring.DirectLimit.of_f

deleted theorem Ring.DirectLimit.of_injective

deleted theorem Ring.DirectLimit.quotientMk_of

deleted def Ring.DirectLimit.ringEquiv

deleted theorem Ring.DirectLimit.ringEquiv_of

deleted theorem Ring.DirectLimit.ringEquiv_symm_mk

deleted def Ring.DirectLimit

Created Mathlib/Algebra/Colimit/Ring.lean

added theorem Field.DirectLimit.exists_inv

added def Ring.DirectLimit.congr

added theorem Ring.DirectLimit.congr_apply_of

added theorem Ring.DirectLimit.congr_symm_apply_of

added theorem Ring.DirectLimit.exists_of

added theorem Ring.DirectLimit.induction_on

added def Ring.DirectLimit.lift

added theorem Ring.DirectLimit.lift_injective

added theorem Ring.DirectLimit.lift_of

added theorem Ring.DirectLimit.lift_unique

added def Ring.DirectLimit.map

added theorem Ring.DirectLimit.map_apply_of

added theorem Ring.DirectLimit.map_comp

added theorem Ring.DirectLimit.map_id

added theorem Ring.DirectLimit.of.zero_exact

added theorem Ring.DirectLimit.of_f

added theorem Ring.DirectLimit.of_injective

added theorem Ring.DirectLimit.quotientMk_of

added def Ring.DirectLimit.ringEquiv

added theorem Ring.DirectLimit.ringEquiv_of

added theorem Ring.DirectLimit.ringEquiv_symm_mk

added def Ring.DirectLimit

Modified Mathlib/Algebra/Homology/LocalCohomology.lean

Modified Mathlib/LinearAlgebra/TensorProduct/DirectLimit.lean

Modified Mathlib/RingTheory/FreeCommRing.lean