instMonoidWithZero

Mathlib.Algebra.Star.StarRingHom

URI: https://scilib.ai/kg/mathlib#NonUnitalStarRingHom.instMonoidWithZero

Lean4

instance : MonoidWithZero (A →⋆ₙ+* A) where
  zero_mul := fun _ => ext fun _ => rfl
  mul_zero := fun f => ext fun _ => map_zero f

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

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

Разделы

Аффилиация

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