consRecOn_ofGroup — Mathlib

English

A specialization of consRecOn showing consistency with ofGroup construction.

Русский

Спецификация consRecOn: совместимо с конструктором ofGroup.

LaTeX

$$$\\mathrm{consRecOn}(\\mathrm{ofGroup\\,g}) = \\mathrm{ofGroup\\,g}$$$

Lean4

@[simp]
theorem consRecOn_ofGroup {motive : NormalWord d → Sort*} (g : G) (ofGroup : ∀ g, motive (ofGroup g))
    (cons :
      ∀ (g : G) (u : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u)
        (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'),
        motive w → motive (cons g u w h1 h2)) :
    consRecOn (.ofGroup g) ofGroup cons = ofGroup g :=
  rfl

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