instIsLocalHomOfMonoidWithZeroHomClassOfNontrivial

English

In a MonoidWithZero, if b and d commute and are nonzero, then a / b = c / d iff a d = c b.

Русский

В моноиде с нулём, если b и d коммутируют и оба ненулевые, то a / b = c / d тогда и только тогда, когда a d = c b.

LaTeX

$$\\forall a,b,c,d\\in G_0,\\ hbd: Commute(b,d), hb: b \\neq 0, hd: d \\neq 0, \\\\; a / b = c / d \\iff a \\cdot d = c \\cdot b$$

Lean4

instance [GroupWithZero G₀] [FunLike F G₀ M₀] [MonoidWithZeroHomClass F G₀ M₀] [Nontrivial M₀] (f : F) : IsLocalHom f :=
  isLocalHom_of_exists_map_ne_one ⟨0, by simp⟩

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