Commensurable — Mathlib

English

Two subgroups H and K of a group G are commensurable if H ∩ K has finite index in both H and K.

Русский

Две подгруппы H и K группы G называются комменсурируемыми, если их пересечение H ∩ K имеет конечный индекс как в H, так и в K.

LaTeX

$$$[H : H \\cap K] < \\infty \\;\\land\\; [K : H \\cap K] < \\infty$$$

Lean4

/-- Two subgroups `H K` of `G` are commensurable if `H ⊓ K` has finite index in both `H` and `K`. -/
@[to_additive /-- Two subgroups `H K` of `G` are commensurable if `H ⊓ K` has finite index in both
    `H` and `K`. -/
    ]
def Commensurable (H K : Subgroup G) : Prop :=
  H.relIndex K ≠ 0 ∧ K.relIndex H ≠ 0

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