English
Basic compatibility of divBy with addition and smul, i.e., divBy is linear and distributes over addition and scalar multiplication.
Русский
Базовая совместимость divBy с суммированием и умножением на скаляры: divBy линейно, распределяется по сложению и по скалярному умножению.
LaTeX
$$$\\mathrm{divBy}(s) \\text{ is an }R\\text{-linear map, i.e. }\\mathrm{divBy}(s)(x+y) = \\mathrm{divBy}(s)x + \\mathrm{divBy}(s)y\\text{ and }\\mathrm{divBy}(s)(r\\cdot x) = r\\cdot(\\mathrm{divBy}(s)x).$$$
Lean4
theorem eq_iff_exists [IsLocalizedModule S f] {x₁ x₂} : f x₁ = f x₂ ↔ ∃ c : S, c • x₁ = c • x₂ :=
Iff.intro exists_of_eq fun ⟨c, h⟩ ↦ by
apply_fun f at h
simp_rw [f.map_smul_of_tower, Submonoid.smul_def, ← Module.algebraMap_end_apply R R] at h
exact ((Module.End.isUnit_iff _).mp <| map_units f c).1 h
