congr — Mathlib

English

If q is obtained from p by a pair of linear equivalences on M and N, i.e., q.compl₁₂ eM.symm eN.symm = p, then q is a perfect pairing.

Русский

Если q получается из p посредством линейных эквивалентностей на M и N, т.е. q = p.compl₁₂ eM.symm eN.symm, то q является совершенной парой.

LaTeX

$$$q.compl₁₂ eM.symm eN.symm = p \Rightarrow q.IsPerfPair$$$

Lean4

theorem congr (eM : M' ≃ₗ[R] M) (eN : N' ≃ₗ[R] N) (q : M' →ₗ[R] N' →ₗ[R] R) (H : q.compl₁₂ eM.symm eN.symm = p) :
    q.IsPerfPair := by
  obtain rfl : q = p.compl₁₂ eM eN := by subst H; ext; simp
  infer_instance

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