extendDomain_mul — Mathlib

English

Extending the domain preserves multiplication: e.extendDomain f · e'.extendDomain f = (e · e').extendDomain f.

Русский

Расширение области определения сохраняет произведение: e.extendDomain f · e'.extendDomain f = (e · e').extendDomain f.

LaTeX

$$$$ e.\extendDomain f \cdot e'.\extendDomain f = (e \cdot e').\extendDomain f. $$$$

Lean4

@[simp]
theorem extendDomain_mul (e e' : Perm α) : e.extendDomain f * e'.extendDomain f = (e * e').extendDomain f :=
  extendDomain_trans _ _ _

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