mulHom_of_of

Mathlib.Algebra.DirectSum.Ring

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

English

If h: IsInternal A for AddSubgroup family A, then iSupIndep A.

Русский

Если A : ι → AddSubgroup имеет IsInternal, то iSupIndep A.

LaTeX

$$IsInternal A \Rightarrow iSupIndep A$$

Lean4

theorem mulHom_of_of {i j} (a : A i) (b : A j) :
    mulHom A (of A i a) (of A j b) = of A (i + j) (GradedMonoid.GMul.mul a b) := by simp

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

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

Разделы

Аффилиация

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