instAlgebraPadic — Mathlib

English

ℂ_p is an algebra over ℚ_p.

Русский

ℂ_p является алгеброй над ℚ_p.

LaTeX

$$$\mathbb{C}_p\quad\text{is an algebra over }\mathbb{Q}_p.$$$

Lean4

/-- `ℂ_[p]` is an algebra over `ℚ_[p]`. -/
instance : Algebra ℚ_[p] ℂ_[p]
    where
  smul := (UniformSpace.Completion.instSMul ℚ_[p] (PadicAlgCl p)).smul
  algebraMap := (UniformSpace.Completion.coeRingHom).comp (algebraMap ℚ_[p] (PadicAlgCl p))
  commutes' r x := by rw [mul_comm]
  smul_def' r
    x := by
    apply UniformSpace.Completion.ext' (continuous_const_smul r) (continuous_mul_left _)
    intro a
    rw [RingHom.coe_comp, Function.comp_apply, Algebra.smul_def]
    rfl

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