diff_mul_diff — Mathlib

English

With the same setup as above, the product of two diff values equals the diff corresponding to the outer pair: diff(ϕ, R, S) · diff(ϕ, S, T) = diff(ϕ, R, T).

Русский

В той же конфигурации произведение двух значений diff равно diff, соответствующему паре на внешней стороне: diff(ϕ,R,S) · diff(ϕ,S,T) = diff(ϕ,R,T).

LaTeX

$$$\operatorname{diff}(\varphi,R,S) \cdot \operatorname{diff}(\varphi,S,T) = \operatorname{diff}(\varphi,R,T)$$$

Lean4

@[to_additive]
theorem diff_mul_diff : diff ϕ R S * diff ϕ S T = diff ϕ R T :=
  prod_mul_distrib.symm.trans
    (prod_congr rfl fun q _ =>
      (ϕ.map_mul _ _).symm.trans (congr_arg ϕ (by simp_rw [Subtype.ext_iff, coe_mul, mul_assoc, mul_inv_cancel_left])))

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