English
There is a canonical IsScalarTower structure for FractionRing over R and intermediary rings.
Русский
Существует каноническая структура IsScalarTower для FractionRing над R и промежуточными кольцами.
LaTeX
$$FractionRing.instIsScalarTower_match_1$$
Lean4
instance (B C : Type*) [CommRing B] [IsDomain B] [CommRing C] [IsDomain C] [Algebra A B] [Algebra A C] [Algebra B C]
[NoZeroSMulDivisors A B] [NoZeroSMulDivisors A C] [NoZeroSMulDivisors B C] [IsScalarTower A B C] :
IsScalarTower (FractionRing A) (FractionRing B) (FractionRing C) where
smul_assoc a b
c :=
a.ind fun ⟨a₁, a₂⟩ ↦ by
rw [← smul_right_inj (nonZeroDivisors.coe_ne_zero a₂)]
simp_rw [← smul_assoc, Localization.smul_mk, smul_eq_mul, Localization.mk_eq_mk',
IsLocalization.mk'_mul_cancel_left, algebraMap_smul, smul_assoc]
