factor_comp — Mathlib

English

For p ≤ p' ≤ p'' and x ∈ M ⧸ p, applying two factors in succession is the same as applying the single factor to x.

Русский

Для p ≤ p' ≤ p'' и x ∈ M/ p, применение двух факторов последовательно эквивалентно применению одного фактора к x.

LaTeX

$$$$ (\\text{factor} \\, H2) (\\text{factor} \\, H1 \\; x) = \\text{factor} (H1.trans H2) \\; x. $$$$

Lean4

@[simp]
theorem factor_comp (H1 : p ≤ p') (H2 : p' ≤ p'') : (factor H2).comp (factor H1) = factor (H1.trans H2) :=
  by
  ext
  simp

Похожие утверждения