Commit 2026-03-25 23:27 a12a22f4

View on Github →

feat(RingTheory/AdicCompletion): completeness of AdicCompletion (#35670) This is the last PR split from #34936, which follows [Stacks 05GG] and formalizes the result that AdicCompletion I M is I-adically complete when the ideal I is finitely generated.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/SModEq/Basic.lean

added theorem SModEq.restrictScalars

Modified Mathlib/RingTheory/AdicCompletion/Basic.lean

added theorem AdicCompletion.pow_smul_top_le_ker_eval

added theorem AdicCompletion.val_apply_mem_smul_top_iff

added theorem IsAdicComplete.map_algebraMap_iff

modified theorem IsHausdorff.map_algebraMap_iff

added theorem IsPrecomplete.map_algebraMap_iff

Created Mathlib/RingTheory/AdicCompletion/Completeness.lean

added theorem AdicCompletion.isAdicComplete

added theorem AdicCompletion.ofPowSMul_injective

added theorem AdicCompletion.ofPowSMul_ofValEqZero

added theorem AdicCompletion.ofPowSMul_val_apply

added theorem AdicCompletion.ofPowSMul_val_apply_eq_zero

added def AdicCompletion.ofValEqZero

added def AdicCompletion.ofValEqZeroAux

added theorem AdicCompletion.pow_smul_top_eq_ker_eval

added theorem AdicCompletion.restrictScalars_range_ofPowSMul_eq_ker_eval