English
Right-multiplicative relation for localization maps.
Русский
Отношение справа для отображений локализации.
LaTeX
$$$ \\text{map\\_mul\\_right}(z) :\\ f.map \\ hy\\ k\\ z \\cdot k (g (f.sec z).2) = k (g (f.sec z).1) $$$
Lean4
/-- Given Localization maps `f : M →* N, k : P →* Q` for Submonoids `S, T` respectively, if a
`CommMonoid` homomorphism `g : M →* P` induces a `f.map hy k : N →* Q`, then for all `z : N`,
we have `k (g y) * f.map hy k z = k (g x)` where `x : M, y ∈ S` are such that
`z * f y = f x`. -/
@[to_additive /-- Given Localization maps `f : M →+ N, k : P →+ Q` for AddSubmonoids `S, T` respectively if an
`AddCommMonoid` homomorphism `g : M →+ P` induces a `f.map hy k : N →+ Q`, then for all `z : N`,
we have `k (g y) + f.map hy k z = k (g x)` where `x : M, y ∈ S` are such that
`z + f y = f x`. -/
]
theorem map_mul_left (z) : k (g (f.sec z).2) * f.map hy k z = k (g (f.sec z).1) := by rw [mul_comm, f.map_mul_right]
