continuousAddCharEquiv_of_norm_mul_apply

English

For κ in the domain, the application of continuousAddCharEquiv_of_norm_mul to κ yields the same κ(1) − 1.

Русский

Применение continuousAddCharEquiv_of_norm_mul к κ даёт то же самое κ(1) − 1.

LaTeX

$$$$\operatorname{continuousAddCharEquiv\_of\_norm\_mul\_apply}~p~R~\langle\kappa,\,h\kappa\rangle = \kappa(1)-1.$$$$

Lean4

@[simp]
theorem continuousAddCharEquiv_of_norm_mul_apply {κ : AddChar ℤ_[p] R} (hκ : Continuous κ) :
    continuousAddCharEquiv_of_norm_mul p R ⟨κ, hκ⟩ = κ 1 - 1 :=
  rfl

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