instMulEquivClass — Mathlib

English

ContinuousMulEquiv M N carries a MulEquivClass structure; the multiplication map is given by f ↦ f.map_mul'.

Русский

ContinuousMulEquiv M N обладает структурой MulEquivClass; операция умножения задается через f.map_mul'.

LaTeX

$$$\text{MulEquivClass}(\mathrm{ContinuousMulEquiv}\,M\,N)\,M\,N\quad\text{with }\mathrm{map\_mul}(f)=f.map\_mul'.$$$

Lean4

@[to_additive]
instance : MulEquivClass (M ≃ₜ* N) M N where map_mul f := f.map_mul'

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