instIsRightCancelMul — Mathlib

English

If M is a right cancellative semigroup, then Germ l M is a right cancellative semigroup; i.e., f2 * f1 = f3 * f1 implies f2 = f3.

Русский

Если M — праворасходящая полугруппа, то Germ l M — правая отменяемая полугруппа; если f2·f1 = f3·f1, то f2 = f3.

LaTeX

$$$ [\\text{RightCancelMul } M] \\Rightarrow [\\text{RightCancelMul } (\\mathrm{Germ}(l, M))]$$$

Lean4

@[to_additive]
instance instIsRightCancelMul [Mul M] [IsRightCancelMul M] : IsRightCancelMul (Germ l M) where
  mul_right_cancel f₁ f₂
    f₃ := inductionOn₃ f₁ f₂ f₃ fun _f₁ _f₂ _f₃ H => coe_eq.2 <| (coe_eq.1 H).mono fun _x => mul_right_cancel

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