English
The lift respects multiplication on the right: f.lift hg z · g(f.sec z).snd = g(f.sec z).fst.
Русский
Подъем сохраняет умножение справа: f.lift hg z · g(f.sec z).snd = g(f.sec z).fst.
LaTeX
$$$ f.lift hg z \cdot g(f.sec z).snd = g(f.sec z).fst $$$
Lean4
/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M`, if a `CommMonoid` map
`g : M →* P` induces a map `f.lift hg : N →* P` then for all `z : N`, we have
`g y * f.lift hg z = g x`, where `x : M, y ∈ S` are such that `z * f y = f x`. -/
@[to_additive /-- Given a Localization map `f : M →+ N` for an AddSubmonoid `S ⊆ M`, if an `AddCommMonoid` map
`g : M →+ P` induces a map `f.lift hg : N →+ P` then for all `z : N`, we have
`g y + f.lift hg z = g x`, where `x : M, y ∈ S` are such that `z + f y = f x`. -/
]
theorem lift_mul_left (z) : g (f.sec z).2 * f.lift hg z = g (f.sec z).1 := by rw [mul_comm, lift_mul_right]
