mulEquivHaarChar_refl — Mathlib

English

The scaling factor for the identity map is 1: mulEquivHaarChar (ContinuousMulEquiv.refl G) = 1.

Русский

Коэффициент масштаба для тождественного отображения равен 1: mulEquivHaarChar (ContinuousMulEquiv.refl G) = 1.

LaTeX

$$$mulEquivHaarChar(ContinuousMulEquiv.refl G) = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem mulEquivHaarChar_refl : mulEquivHaarChar (ContinuousMulEquiv.refl G) = 1 := by
  simp [mulEquivHaarChar, Function.id_def]

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