English
If P and Q are submodules with a map induced by the identity, the quotient equivalence built from this map equals the quotient equivalence coming from the equality P = Q.
Русский
Если P и Q — подмодули и есть отображение между их частями, индуцированное тождеством, то эквивалентность по фактор-модулям, полученная из этого отображения, совпадает с эквивалентностью, полученной из равенства P = Q.
LaTeX
$$$\text{If } hf: P.map(\mathrm{Id}) = Q, \; \Quotient.equiv P Q (\mathrm{Id}) hf = \quotEquivOfEq P Q (by simpa using hf).$$$
Lean4
@[simp]
theorem equiv_refl (P : Submodule R M) (Q : Submodule R M) (hf : P.map (LinearEquiv.refl R M : M →ₗ[R] M) = Q) :
Quotient.equiv P Q (LinearEquiv.refl R M) hf = quotEquivOfEq _ _ (by simpa using hf) :=
rfl
