Skip to content

refactor(RepresentationTheory/FiniteIndex): simpler design of indToCoindAux using ind.lift - #44265

Open
JX-Mo wants to merge 4 commits into
leanprover-community:masterfrom
JX-Mo:Representation.FiniteIndex
Open

refactor(RepresentationTheory/FiniteIndex): simpler design of indToCoindAux using ind.lift#44265
JX-Mo wants to merge 4 commits into
leanprover-community:masterfrom
JX-Mo:Representation.FiniteIndex

Commits

  1. Commits on Sep 27, 2026

    • fix

      JX-MoJX-Mo
      committed
      d555173

    • fix

      JX-MoJX-Mo
      committed
      f43fbc1

  2. Commits on Sep 29, 2026

  3. Commits on Oct 27, 2026