RightTransversal — Mathlib

English

The collection of right transversals of a subgroup is the set of T ⊆ G such that H and T form a right complement.

Русский

Собрание правых трансверсалів — множество T ⊆ G так, что H и T образуют правый комплемент.

LaTeX

$$Abbrev: RightTransversal (H) := { T : Set G // IsComplement H T }$$

Lean4

/-- The collection of right transversals of a subgroup -/
@[to_additive /-- The collection of right transversals of a subgroup. -/
    ]
abbrev RightTransversal (H : Subgroup G) :=
  { T : Set G // IsComplement H T }

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