Commit 2023-02-23 08:11 6ae4a72f

View on Github →

feat: Port/Data.QPF.Multivariate.Constructions.Fix (#2409)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean

added def MvQPF.Fix.dest

added theorem MvQPF.Fix.dest_mk

added def MvQPF.Fix.drec

added theorem MvQPF.Fix.ind

added theorem MvQPF.Fix.ind_aux

added theorem MvQPF.Fix.ind_rec

added def MvQPF.Fix.map

added def MvQPF.Fix.mk

added theorem MvQPF.Fix.mk_dest

added def MvQPF.Fix.rec

added theorem MvQPF.Fix.rec_eq

added theorem MvQPF.Fix.rec_unique

added def MvQPF.Fix

added inductive MvQPF.WEquiv

added def MvQPF.fixToW

added def MvQPF.recF

added theorem MvQPF.recF_eq'

added theorem MvQPF.recF_eq

added theorem MvQPF.recF_eq_of_wEquiv

added theorem MvQPF.wEquiv.abs'

added theorem MvQPF.wEquiv.refl

added theorem MvQPF.wEquiv.symm

added theorem MvQPF.wEquiv_map

added def MvQPF.wSetoid

added def MvQPF.wrepr

added theorem MvQPF.wrepr_equiv

added theorem MvQPF.wrepr_wMk