ofUnits_sup_units — Mathlib

English

The units of the sum of two subgroups equal the sum of the units: (S.ofUnits ⊔ T.ofUnits).units = S ⊔ T.

Русский

Единицы объединения подгрупп равны объединению единиц: (S.ofUnits ⊔ T.ofUnits).units = S ⊔ T.

LaTeX

$$$ (S^{\\mathrm{ofUnits}} \\lor T^{\\mathrm{ofUnits}})^{\\mathrm{units}} = S \\lor T $$$

Lean4

@[to_additive (attr := simp)]
theorem ofUnits_sup_units (S T : Subgroup Mˣ) : (S.ofUnits ⊔ T.ofUnits).units = S ⊔ T :=
  ofUnits_units_gci.u_sup_l _ _

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