isCancelMul — Mathlib

English

If M is cancellative and f : S.LocalizationMap N is a localization map, then N is cancellative as well.

Русский

Если M удовлетворяет свойству отмены и имеется локализационная карта f, то и N удовлетворяет свойству отмены.

LaTeX

$$$\\text{IsCancelMul}(N)$ given $f : S. LocalizationMap \\ N$ and $\\text{IsCancelMul}(M)$$$

Lean4

@[to_additive]
theorem isCancelMul (f : LocalizationMap S N) [IsCancelMul M] : IsCancelMul N :=
  by
  simp_rw [isCancelMul_iff_forall_isRegular, Commute.isRegular_iff (Commute.all _), ←
    Commute.isRightRegular_iff (Commute.all _)]
  intro n
  have ⟨ms, eq⟩ := f.surj n
  exact (eq ▸ f.map_isRegular (isCancelMul_iff_forall_isRegular.mp ‹_› ms.1)).2.of_mul

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