instNontrivial

Mathlib.Algebra.Group.Subgroup.Lattice

URI: https://scilib.ai/kg/mathlib#Subgroup.instNontrivial

English

If G is nontrivial, then Subgroup G is nontrivial.

Русский

Если G ненольная, то подпгруппа G ненольная.

LaTeX

$$[If\: Nontrivial(G) then Nontrivial(Subgroup(G))]$$

Lean4

@[to_additive]
instance [Nontrivial G] : Nontrivial (Subgroup G) :=
  nontrivial_iff.mpr ‹_›

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru