ofUnits_inf — Mathlib

English

The ofUnits of the join of two subgroups of units equals the join of their respective ofUnits.

Русский

Объединение единиц сохранится под образованием ofUnits: (S ⊔ T).ofUnits = S.ofUnits ⊔ T.ofUnits.

LaTeX

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

Lean4

@[to_additive]
theorem ofUnits_inf (S T : Subgroup Mˣ) : (S ⊔ T).ofUnits = S.ofUnits ⊔ T.ofUnits :=
  ofUnits_units_gc.l_sup

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