congr — Mathlib

English

Baer property is invariant under linear equivalence: Module.Baer R Q ↔ Module.Baer R M when Q ≃ℓ[R] M.

Русский

Свойство Баера сохраняется при линейном эквивалентном отображении: Module.Baer R Q ↔ Module.Baer R M при Q ≃ℓ[R] M.

LaTeX

$$$ \text{Module.Baer } R Q \leftrightarrow \text{Module.Baer } R M$$$

Lean4

theorem congr (e : Q ≃ₗ[R] M) : Module.Baer R Q ↔ Module.Baer R M :=
  ⟨of_equiv e, of_equiv e.symm⟩

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