continuousAddCharEquiv_apply — Mathlib

English

For any κ, hκ continuous, the applied form of the equivalence satisfies continuousAddCharEquiv_apply: continuousAddCharEquiv p R ⟨κ,hκ⟩ = κ 1 − 1.

Русский

Для любого κ с непрерывностью применимая часть эквивалентности даёт continuousAddCharEquiv p R ⟨κ,hκ⟩ = κ(1) − 1.

LaTeX

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

Lean4

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

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