toAddMonoid_inj

Mathlib.Algebra.DirectSum.Basic

URI: https://scilib.ai/kg/mathlib#DirectSum.toAddMonoid_inj

English

The equivalence toAddMonoid f = toAddMonoid g iff f = g.

Русский

Эквивалентность toAddMonoid f = toAddMonoid g эквивалентна f = g.

LaTeX

$$toAddMonoid_inj$$

Lean4

@[simp]
theorem toAddMonoid_inj {f g : ∀ i, β i →+ γ} : toAddMonoid f = toAddMonoid g ↔ f = g :=
  toAddMonoid_injective.eq_iff

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

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

Разделы

Аффилиация

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