quotIntNorm_apply — Mathlib

English

For any a in integerSet K, the quotient-norm evaluation equals the integer-set norm: quotIntNorm(⟦a⟧) = intNorm(a).

Русский

Для любого a из integerSet K выполнение quotIntNorm на соответствующем классе эквивалентности равно intNorm(a).

LaTeX

$$$\\quotIntNorm(\\llbracket a \\rrbracket) = \\operatorname{intNorm}(a).$$$

Lean4

@[simp]
theorem quotIntNorm_apply (a : integerSet K) : quotIntNorm ⟦a⟧ = intNorm a :=
  rfl

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