Commit 2023-05-18 11:07 4c76d314

View on Github →

feat: port RingTheory.Ideal.LocalRing (#4066)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Ideal/LocalRing.lean

added theorem LocalRing.ResidueField.algebraMap_eq

added def LocalRing.ResidueField.lift

added theorem LocalRing.ResidueField.lift_comp_residue

added theorem LocalRing.ResidueField.lift_residue_apply

added def LocalRing.ResidueField.map

added def LocalRing.ResidueField.mapAut

added theorem LocalRing.ResidueField.mapEquiv.symm

added def LocalRing.ResidueField.mapEquiv

added theorem LocalRing.ResidueField.mapEquiv_refl

added theorem LocalRing.ResidueField.mapEquiv_trans

added theorem LocalRing.ResidueField.map_comp

added theorem LocalRing.ResidueField.map_comp_residue

added theorem LocalRing.ResidueField.map_id

added theorem LocalRing.ResidueField.map_id_apply

added theorem LocalRing.ResidueField.map_map

added theorem LocalRing.ResidueField.map_residue

added theorem LocalRing.ResidueField.residue_smul

added def LocalRing.ResidueField

added theorem LocalRing.eq_maximalIdeal

added theorem LocalRing.isField_iff_maximalIdeal_eq

added theorem LocalRing.isLocalRingHom_residue

added theorem LocalRing.isUnit_of_mem_nonunits_one_sub_self

added theorem LocalRing.isUnit_one_sub_self_of_mem_nonunits

added theorem LocalRing.isUnit_or_isUnit_of_isUnit_add

added theorem LocalRing.isUnit_or_isUnit_one_sub_self

added theorem LocalRing.jacobson_eq_maximalIdeal

added theorem LocalRing.ker_eq_maximalIdeal

added theorem LocalRing.le_maximalIdeal

added theorem LocalRing.local_hom_TFAE

added def LocalRing.maximalIdeal

added theorem LocalRing.maximalIdeal_eq_bot

added theorem LocalRing.maximal_ideal_unique

added theorem LocalRing.mem_maximalIdeal

added theorem LocalRing.nonunits_add

added theorem LocalRing.of_isUnit_or_isUnit_of_isUnit_add

added theorem LocalRing.of_isUnit_or_isUnit_one_sub_self

added theorem LocalRing.of_nonunits_add

added theorem LocalRing.of_surjective'

added theorem LocalRing.of_surjective

added theorem LocalRing.of_unique_max_ideal

added theorem LocalRing.of_unique_nonzero_prime

added def LocalRing.residue

added theorem LocalRing.surjective_units_map_of_local_ringHom

added theorem RingHom.domain_localRing

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