coe_trans_mulEquiv — Mathlib

English

The MulEquiv underlying f.trans g equals the transitive composition of the MulEquiv underlying f and g.

Русский

Лежащая в основе MulEquiv для f.trans g равна композиции MulEquiv f и MulEquiv g.

LaTeX

$$$MulEquivClass.toMulEquiv (f.trans g) = (MulEquivClass.toMulEquiv f).trans (MulEquivClass.toMulEquiv g)$$$

Lean4

@[to_additive]
theorem coe_trans_mulEquiv (f : α ≃*o β) (g : β ≃*o γ) : (f.trans g : α ≃* γ) = (f : α ≃* β).trans g :=
  rfl

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