rightCoset_one

Mathlib.GroupTheory.Coset.Basic

URI: https://scilib.ai/kg/mathlib#rightCoset_one

English

Multiplying on the left by the identity in the opposite sense leaves cosets unchanged: op(1)•s = s.

Русский

Умножение слева единицей в противоположном смысле не меняет косеты: op(1)•s = s.

LaTeX

$$op(1) • s = s$$

Lean4

@[to_additive rightAddCoset_zero]
theorem rightCoset_one : op (1 : α) • s = s :=
  Set.ext <| by simp

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

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

Разделы

Аффилиация

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