refl_toLinearEquiv

Mathlib.RingTheory.Coalgebra.Equiv

URI: https://scilib.ai/kg/mathlib#CoalgEquiv.refl_toLinearEquiv

English

The identity coalgebra equivalence coincides with the identity linear equivalence.

Русский

Коалгебраическая эквивалентность-идентичность совпадает с линейной эквивалентностью-идентичностью.

LaTeX

$$$\\text{refl } R\\; A = \\text{LinearEquiv.refl } R\\; A$$$

Lean4

@[simp]
theorem refl_toLinearEquiv : refl R A = LinearEquiv.refl R A :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru