English
The same statement with the factors commuted: localizing away from x*y is equivalent to localizing away from y*x.
Русский
То же самое после перестановки множителей: локализация away от x*y эквивалентна локализации away от y*x.
LaTeX
$$$IsLocalization.Away (x \\cdot y) T = IsLocalization.Away (y \\cdot x) T$$$
Lean4
/-- Localizing the localization of `R` at `x` at the image of `y` is the same as localizing
`R` at `x * y`. See `IsLocalization.Away.mul` for the `y * x` version. -/
theorem mul' (T : Type*) [CommSemiring T] [Algebra S T] [Algebra R T] [IsScalarTower R S T] (x y : R)
[IsLocalization.Away x S] [IsLocalization.Away (algebraMap R S y) T] : IsLocalization.Away (x * y) T :=
mul_comm x y ▸ mul S T x y
