instIsLeftCancelMul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
instance instIsLeftCancelMul [Mul M] [IsLeftCancelMul M] : IsLeftCancelMul (Germ l M) where
  mul_left_cancel f₁ f₂
    f₃ := inductionOn₃ f₁ f₂ f₃ fun _f₁ _f₂ _f₃ H => coe_eq.2 ((coe_eq.1 H).mono fun _x => mul_left_cancel)

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