Theorems · Definition · commutative algebra

AdicCompletion.mk

{R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] → AdicCompletion.AdicCauchySequence I M →ₗ[R] AdicCompletion I M

The canonical linear map from Cauchy sequences to the completion.

Defined in: Mathlib.RingTheory.AdicCompletion.Basic
Cited by: 22 results in Mathlib
Foundations: Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing AddCommGroup Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Modulestatement and proof · cited by 20,661
RingHom.idstatement · cited by 18,349
CommRingstatement and proof · cited by 17,173
AddCommGroupstatement and proof · cited by 12,871
LinearMapstatement · cited by 10,215
Top.topproof · cited by 9,680
Idealstatement and proof · cited by 4,748
Submodule.mkQproof · cited by 232
AdicCompletionstatement · cited by 160
AdicCompletion.AdicCauchySequencestatement and proof · cited by 41

Cited by23

Results whose statement or proof uses this declaration.

AdicCompletion.mk_apply_coestatement and proof · cited by 10
AdicCompletion.induction_onstatement and proof · cited by 9
AdicCompletion.map_ext'statement and proof · cited by 6
AdicCompletion.map_surjectiveproof · cited by 2
AdicCompletion.mkₐproof · cited by 2
AdicCompletion.map_injectiveproof · cited by 1
AdicCompletion.map_surjective_of_mkQ_comp_surjectiveproof · cited by 1
AdicCompletion.map_zeroproof · cited by 1
AdicCompletion.mk_surjectivestatement · cited by 1
AdicCompletion.mk_zero_ofstatement · cited by 1
AdicCompletion.sumInv_applyproof · cited by 1
AdicCompletion.component_sumInvproof · cited by 1