basisQuotient_apply — Mathlib

English

For a basis b of S, the i-th element of the quotient basis is the image of b_i under the quotient map to S/pS.

Русский

Пусть b — базис S; i-я компонента базиса в S/ pS равна образу b_i по отношению к фактор-модулю.

LaTeX

$$$(basisQuotient\, b)\\, i = \\mathrm{Ideal.Quotient.mk} \\, p_S (b\\, i)$$$

Lean4

theorem basisQuotient_apply [Fintype ι] (b : Basis ι R S) (i) : (basisQuotient b) i = Ideal.Quotient.mk pS (b i) :=
  by
  delta basisQuotient
  rw [coe_basisOfTopLeSpanOfCardEqFinrank, Function.comp_apply]

Похожие утверждения