groupNormClass — Mathlib

English

There exists a GroupNormClass instance for GroupNorm E, ensuring compatibility of map, multiplication and inversion with the norm structure.

Русский

Существует экземпляр GroupNormClass для GroupNorm E, обеспечивающий совместимость отображения, умножения и инверсии с конструкцией нормы.

LaTeX

$$$ \text{GroupNorm} \text{class} : \mathrm{GroupNormClass}(\mathrm{GroupNorm}(E)) $$$

Lean4

@[to_additive]
instance groupNormClass : GroupNormClass (GroupNorm E) E ℝ
    where
  map_one_eq_zero f := f.map_one'
  map_mul_le_add f := f.mul_le'
  map_inv_eq_map f := f.inv'
  eq_one_of_map_eq_zero f := f.eq_one_of_map_eq_zero' _

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