on_isRefl — Mathlib

English

If f: G → S and S is a multiplication structure, then the pullback Commute along f is reflexive: Commute (f a) (f a) for all a.

Русский

Если f: G → S и S имеет умножение, то соответствующее отношение коммутирования на образе f является рефлексивным: Commute (f a) (f a) для всех a.

LaTeX

$$$\\forall a \\in G,\\ Commute (f a) (f a)$$$

Lean4

@[to_additive]
instance on_isRefl {f : G → S} : IsRefl G fun a b => Commute (f a) (f b) :=
  ⟨fun _ => Commute.refl _⟩

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