Theorems · Theorem · commutative algebra
IsLocalization.Away.mul
∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (T : Type u_5)
[inst_3 : CommSemiring T] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [IsScalarTower R S T] (x y : R)
[IsLocalization.Away x S] [IsLocalization.Away ((algebraMap R S) y) T], IsLocalization.Away (y * x) TLocalizing the localization of R at x at the image of y is the same as localizing
R at y * x. See IsLocalization.Away.mul' for the x * y version.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- RingHomstatement · cited by 10,189
- Algebra.algebraMapstatement and proof · cited by 4,706
- IsScalarTowerstatement and proof · cited by 3,896
- IsUnitproof · cited by 1,602
- map_mulproof · cited by 1,137
- map_powproof · cited by 503
- pow_addproof · cited by 315
- mul_powproof · cited by 220
- IsLocalization.Awaystatement and proof · cited by 218
Cited by4
Results whose statement or proof uses this declaration.
- IsLocalization.Away.mul'proof · cited by 7
- Algebra.IsStandardEtale.of_isLocalizationAwayproof · cited by 2
- Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂proof · cited by 1
- IsLocalization.Away.mul_of_isUnit'proof · cited by 0