quotients-and-lifts

Work effectively with Lean 4 quotients in ComputationalPaths (Quot.lift/Quot.ind/Quot.sound), including nested lifts and common proof obligations.

by Arthur742Ramos· Repository·development
quotients
and
lifts
Also installable via skills CLI
npx skills add Arthur742Ramos/ComputationalPathsLean/development/quotients-and-lifts

Source

Repo:local
Path:development/quotients-and-lifts(main)

Related in development