zero_symm — Mathlib

English

In LinearEquiv over a pair of rings with Subsingleton domains, the symmetry of the zero equivalence is itself the zero equivalence.

Русский

В линейной эквивалентности над парами колец, когда домены поля сведены к одному элементу, симметрия нулевой эквивалентности равна нулевой эквивалентности.

LaTeX

$$$$ (0 : M \\simeq_{σ_{12}} M_2)^{\\mathrm{symm}} = 0 $$$$

Lean4

@[simp]
theorem zero_symm : (0 : M ≃ₛₗ[σ₁₂] M₂).symm = 0 :=
  rfl

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