Commit 2023-07-03 07:59 f3e62849

View on Github →

feat: port Data.QPF.Multivariate.Constructions.Cofix (#2444)

Estimated changes

Modified Mathlib.lean

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

added def MvQPF.Cofix.abs

added theorem MvQPF.Cofix.abs_repr

added theorem MvQPF.Cofix.bisim'

added theorem MvQPF.Cofix.bisim

added theorem MvQPF.Cofix.bisim_rel

added theorem MvQPF.Cofix.bisim₂

added def MvQPF.Cofix.corec'

added def MvQPF.Cofix.corec'₁

added def MvQPF.Cofix.corec

added def MvQPF.Cofix.corec₁

added def MvQPF.Cofix.dest

added theorem MvQPF.Cofix.dest_corec'

added theorem MvQPF.Cofix.dest_corec

added theorem MvQPF.Cofix.dest_corec₁

added theorem MvQPF.Cofix.dest_mk

added theorem MvQPF.Cofix.ext

added theorem MvQPF.Cofix.ext_mk

added def MvQPF.Cofix.map

added def MvQPF.Cofix.mk

added theorem MvQPF.Cofix.mk_dest

added def MvQPF.Cofix.repr

added def MvQPF.Cofix

added def MvQPF.IsPrecongr

added def MvQPF.Mcongr

added def MvQPF.corecF

added theorem MvQPF.corecF_eq

added theorem MvQPF.corec_roll

added theorem MvQPF.liftR_map

added theorem MvQPF.liftR_map_last'

added theorem MvQPF.liftR_map_last

added def MvQPF.mRepr