English
The formula for quotTensorEquivQuotSMul_mk_tmul gives the image of (I) mk r ⊗ x as the class of r•x.
Русский
Формула quotTensorEquivQuotSMul_mk_tmul задаёт образ (I) mk r ⊗ x как класс r·x.
LaTeX
$$$$ \text{quotTensorEquivQuotSMul}_M I \big( \text{Ideal.Quotient.mk } I r \otimes x \big) = \text{Submodule.Quotient.mk} (r \cdot x). $$$$
Lean4
/-- Let `R` be a commutative ring, `S` be an `R`-algebra, `I` is be ideal of `R`, then `S ⧸ IS` is
isomorphic to `S ⊗[R] (R ⧸ I)` as `S` modules. -/
noncomputable def _root_.Ideal.qoutMapEquivTensorQout {I : Ideal R} : (S ⧸ I.map (algebraMap R S)) ≃ₗ[S] S ⊗[R] (R ⧸ I)
where
__ :=
LinearEquiv.symm <|
tensorQuotEquivQuotSMul S I ≪≫ₗ Submodule.quotEquivOfEq _ _ (by simp) ≪≫ₗ
Submodule.Quotient.restrictScalarsEquiv R _
map_smul' := by
rintro _ ⟨_⟩
congr
