instNonarchimedeanGroup — Mathlib

English

The Cartesian product of two nonarchimedean groups is nonarchimedean.

Русский

Декартово произведение двух неархимедовых групп неархимедово.

LaTeX

$$NonarchimedeanGroup (G × K)$$

Lean4

/-- The Cartesian product of two nonarchimedean groups is nonarchimedean. -/
@[to_additive /-- The Cartesian product of two nonarchimedean groups is nonarchimedean. -/
    ]
instance instNonarchimedeanGroup : NonarchimedeanGroup (G × K) where
  is_nonarchimedean _
    hU :=
    let ⟨V, W, h⟩ := prod_subset hU
    ⟨V.prod W, ‹_›⟩

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