Commit 2024-05-18 21:23 fa9ce74b

View on Github →

feat(RingTheory/AdicCompletion): add algebra instance (#12553) Adds the algebra instance on the I-adic completion of a ring R. Also provides the AdicCompletion I R-module instance on AdicCompletion I M for every R-module M.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Torsion.lean

added theorem Module.Quotient.mk_smul_mk

Modified Mathlib/LinearAlgebra/SModEq.lean

added theorem SModEq.mul

Created Mathlib/RingTheory/AdicCompletion/Algebra.lean

added def AdicCompletion.AdicCauchySequence.subalgebra

added def AdicCompletion.AdicCauchySequence.subring

added theorem AdicCompletion.Ideal.mk_eq_mk

added def AdicCompletion.evalₐ

added theorem AdicCompletion.evalₐ_mk

added theorem AdicCompletion.evalₐ_mkₐ

added theorem AdicCompletion.mk_smul_mk

added def AdicCompletion.mkₐ

added theorem AdicCompletion.mul_apply

added theorem AdicCompletion.one_apply

added theorem AdicCompletion.smul_eval

added theorem AdicCompletion.smul_mk

added def AdicCompletion.subalgebra

added def AdicCompletion.subring

added theorem AdicCompletion.transitionMap_ideal_mk

added theorem AdicCompletion.transitionMap_map_mul

added theorem AdicCompletion.transitionMap_map_one

added def AdicCompletion.transitionMapₐ

added theorem AdicCompletion.val_mul

added theorem AdicCompletion.val_one

Modified Mathlib/RingTheory/AdicCompletion/Basic.lean

added theorem AdicCompletion.AdicCauchySequence.mk_eq_mk