coe_quotientInfToSupQuotient — Mathlib

English

Equality of the function behind quotientInfToSupQuotient with its canonical form.

Русский

Равенство функции quotientInfToSupQuotient и её канонической формы.

LaTeX

$$theorem coe_quotientInfToSupQuotient (p p' : Submodule R M) : ⇑(quotientInfToSupQuotient p p') = quotientInfEquivSupQuotient p p'$$

Lean4

@[simp]
theorem coe_quotientInfToSupQuotient (p p' : Submodule R M) :
    ⇑(quotientInfToSupQuotient p p') = quotientInfEquivSupQuotient p p' :=
  rfl

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