English
If M is a cancellative monoid with zero and f: LocalizationMap S N is a localization map, then N is also cancellative with zero.
Русский
Если M — отменимый моноид с нулём, и f — локализационная карта, то N тоже является отменимым моноидом с нулём.
LaTeX
$$IsCancelMulZero N$$
Lean4
/-- Given a Localization map `f : M →*₀ N` for a Submonoid `S ⊆ M`,
if `M` is a cancellative monoid with zero, and all elements of `S` are
regular, then N is a cancellative monoid with zero. -/
theorem isCancelMulZero (f : LocalizationMap S N) [IsCancelMulZero M] : IsCancelMulZero N :=
by
simp_rw [isCancelMulZero_iff_forall_isRegular, Commute.isRegular_iff (Commute.all _), ←
Commute.isRightRegular_iff (Commute.all _)]
intro n hn
have ⟨ms, eq⟩ := f.surj n
refine (eq ▸ f.map_isRegular (isCancelMulZero_iff_forall_isRegular.mp ‹_› ?_)).2.of_mul
refine fun h ↦ hn ?_
rwa [h, f.map_zero, (f.map_units _).mul_left_eq_zero] at eq
