Commit 2025-02-20 17:05 f94b7dd9

View on Github →

feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal (#21900) Define transtition map between ring or module quotient by powers of ideal, both for developing API for IsAdicComplete

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Quotient/Basic.lean

added theorem Submodule.factor_comp

added theorem Submodule.factor_comp_apply

added theorem Submodule.factor_comp_mk

added theorem Submodule.factor_mk

added theorem Submodule.factor_surjective

Modified Mathlib/RingTheory/AdicCompletion/Algebra.lean

Modified Mathlib/RingTheory/AdicCompletion/Basic.lean

deleted def AdicCompletion.transitionMap

deleted theorem AdicCompletion.transitionMap_comp

deleted theorem AdicCompletion.transitionMap_comp_apply

deleted theorem AdicCompletion.transitionMap_eq

deleted theorem AdicCompletion.transitionMap_mk

Modified Mathlib/RingTheory/Ideal/Quotient/Defs.lean

added theorem Ideal.Quotient.factor_comp

added theorem Ideal.Quotient.factor_comp_apply

added theorem Ideal.Quotient.factor_eq

added theorem Ideal.Quotient.factor_surjective

Created Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean

added theorem Ideal.Quotient.factor_ker

added theorem Submodule.mapQ_eq_factor

added theorem Submodule.pow_smul_top_le