bot_prod_bot — Mathlib

English

The product of bottom subgroups is bottom: (⊥ : Subgroup G).prod (⊥ : Subgroup N) = ⊥.

Русский

Произведение нижних подгрупп равно нижней: (⊥ : Subgroup G).prod (⊥ : Subgroup N) = ⊥.

LaTeX

$$$ (\bot : \mathrm Subgroup G).prod (\bot : \mathrm Subgroup N) = \bot $$$

Lean4

@[to_additive (attr := simp) bot_prod_bot]
theorem bot_prod_bot : (⊥ : Subgroup G).prod (⊥ : Subgroup N) = ⊥ :=
  SetLike.coe_injective <| by simp [coe_prod]

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