symm_apply — Mathlib

English

The EquivLike structure on CoalgEquiv ensures that equality is determined by the action on inputs.

Русский

Структура EquivLike на CoalgEquiv обеспечивает, что равенство определяется действием на входах.

LaTeX

$$$\\text{ext} \\; (h: \\forall x, e(x) = e'(x)) \\Rightarrow e = e'$$$

Lean4

/-- See Note [custom simps projection] -/
def symm_apply {R : Type*} [CommSemiring R] {A : Type*} {B : Type*} [AddCommMonoid A] [AddCommMonoid B] [Module R A]
    [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : B → A :=
  e.symm

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