Commit 2024-07-19 18:48 736794fe

View on Github →

chore: Split and move RingTheory.Ideal.LocalRing (#14829) Currently, LocalRing is defined in the (long) file Mathlib.RingTheory.Ideal.LocalRing. We also have a folder Mathlib.RingTheory.LocalRing that contains only one (advanced) file Module. The file Mathlib.RingTheory.Ideal.LocalRing is moved an splitted in several files. The new structure is

├── RingTheory.LocalRing
│   ├── MaximalIdeal
│   │   ├── Defs
│   │   ├── Basic
│   ├── RingHom
│   │   ├── Defs
│   │   ├── Basic
│   ├── ResidueField
│   │   ├── Defs
│   │   ├── Basic
│   ├── Defs
│   ├── Basic
└── ...

Estimated changes

deleted theorem LocalRing.eq_maximalIdeal
deleted theorem LocalRing.ker_residue
deleted theorem LocalRing.le_maximalIdeal
deleted theorem LocalRing.local_hom_TFAE
deleted theorem LocalRing.nonunits_add
deleted theorem LocalRing.of_nonunits_add
deleted theorem LocalRing.of_surjective'
deleted theorem LocalRing.of_surjective
deleted def LocalRing.residue
deleted theorem RingHom.domain_localRing
deleted theorem isLocalRingHom_of_comp
deleted theorem isUnit_map_iff
deleted theorem isUnit_of_map_unit
deleted theorem map_mem_nonunits_iff
deleted theorem map_nonunit
deleted theorem of_irreducible_map
added theorem LocalRing.nonunits_add
added theorem LocalRing.ker_residue
added theorem isLocalRingHom_of_comp
added theorem isUnit_map_iff
added theorem isUnit_of_map_unit
added theorem map_mem_nonunits_iff
added theorem map_nonunit
added theorem of_irreducible_map