star_sub

Mathlib.Algebra.Star.Basic

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

English

For all r, s in an additive group with star, star(r − s) = star(r) − star(s).

Русский

Для всех r, s в группе с операцией звезды выполняется star(r − s) = star(r) − star(s).

LaTeX

$$$$ (r - s)^{*} = r^{*} - s^{*}. $$$$

Lean4

@[simp]
theorem star_sub [AddGroup R] [StarAddMonoid R] (r s : R) : star (r - s) = star r - star s :=
  (starAddEquiv : R ≃+ R).map_sub _ _

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

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

Разделы

Аффилиация

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