Theorems · Theorem · commutative algebra

Ideal.Quotient.factor_comp_apply

∀ {R : Type u} [inst : Ring R] {S T U : Ideal R} [inst_1 : S.IsTwoSided] [inst_2 : T.IsTwoSided] [inst_3 : U.IsTwoSided]
  (H1 : S ≤ T) (H2 : T ≤ U) (x : R ⧸ S),
  (Ideal.Quotient.factor H2) ((Ideal.Quotient.factor H1) x) = (Ideal.Quotient.factor ⋯) x

Defined in: Mathlib.RingTheory.Ideal.Quotient.Defs
Cited by: 5 results in Mathlib
Foundations: Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Ring Ideal.IsTwoSided Ideal.IsTwoSided Ideal.IsTwoSided

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites10

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

DFunLike.coestatement and proof · cited by 62,936
RingHomstatement · cited by 10,189
Ringstatement and proof · cited by 7,463
Idealstatement and proof · cited by 4,748
LE.le.transstatement and proof · cited by 3,151
HasQuotient.Quotientstatement and proof · cited by 2,301
Ideal.IsTwoSidedstatement and proof · cited by 179
RingHom.comp_applyproof · cited by 41
Ideal.Quotient.factorstatement and proof · cited by 33
Ideal.Quotient.factor_compproof · cited by 1

Cited by5

Results whose statement or proof uses this declaration.

AdicCompletion.evalₐ_liftRingHomproof · cited by 4
Algebra.FormallySmooth.exists_adicCompletionEvalOneₐ_comp_eqproof · cited by 2
AdicCompletion.ker_evalOneₐ_eq_mapproof · cited by 1
AdicCompletion.factor_eval_liftRingHomproof · cited by 0
AdicCompletion.factor_evalₐ_eq_evalproof · cited by 0