Commit 2026-05-31 18:17 7ab72405

View on Github →

feat(RingTheory): AdicCompletion of local ring is local (#37975) In this PR, we proved that AdicCompletion of local ring wrt the maximal ideal is local ring with maximal ideal equal to the map of the original maximal ideal. Also, removing some old junk produced by myself.

Estimated changes

Modified Mathlib/RingTheory/AdicCompletion/Algebra.lean

added theorem AdicCompletion.evalOneₐ_comp_algebraMap_eq_mk

Modified Mathlib/RingTheory/AdicCompletion/Completeness.lean

added theorem AdicCompletion.ker_evalOneₐ_eq_map

Modified Mathlib/RingTheory/AdicCompletion/LocalRing.lean

added theorem AdicCompletion.algebraMap_isLocalHom_of_fg

added theorem AdicCompletion.isAdicComplete_of_fg

added theorem AdicCompletion.isAdicComplete_self

added theorem AdicCompletion.isLocalRing_of_fg

added theorem AdicCompletion.isMaximal_map_of_le

added theorem AdicCompletion.maximalIdeal_eq_map

added theorem AdicCompletion.maximalIdeal_eq_map_of_fg

added theorem AdicCompletion.mem_maximalIdeal_iff_eval_one_eq_zero

added theorem AdicCompletion.residueField_map_bijective

added theorem AdicCompletion.residueField_map_bijective_of_fg

added theorem AdicCompletion.spanFinrank_maximalIdeal_eq

modified theorem isLocalRing_of_isAdicComplete_maximal