Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • Subset
  • essais-8.18
  • master default protected
  • no_ms
  • pr_no_math-comp
  • released
  • test_skolem_ko
  • PhD_HM_2024
  • 1.0
  • Bochner.1.0
  • Tonelli.1.0
  • LInt_p.1.0
12 results
Created with Raphaël 2.2.06May54329Apr28272625232221201915141312118765431Mar30292825242322211817161110986432128Feb26252423222120191817161514131211109876543129Jan2827262524232221201918Rename compl_seq into complf_seq, and mix_seq into mixf_seq.Rename complf_any into complf_fun_any, and mixf_any into mixf_fun_any.Change order.Change order.Done.Extract todo's into TODO file.Extract todo's into TODO file.WIP: unify any/finite/seq.define cur_to_ref_inv, theta_cur and interp_op_local_cur.WIP: lemma pow_bBijective_bInjective_l...renamed sum_n.v to sum_pn.Vchange sum_n to sum_pn and remove zero case in Finite_dim.vWIP: filling empty proofs.Propagate new API.Renaming: <op>_disj*_compat* -> disj*_<op>*.add sum_pn_scal lemma in sum_n.vMv pb...Renaming: <op>_partition*_compat* -> partition*_<op>*.define vertex_ref from T_geom defWIP: filling empty proofs + some renaming.WIP: filling empty proofs about P-any.try to proof shape_fun_lin_indepmix_any (= union) is useless!mix_any is actually union!union_any_mix_any was actually union_union_any_distr, andWIP: filling empty proofs (fix statements).WIP: filling some empty proofs (and add more generic results).Add alternate compl*_invol results.Réunion 3 maiFill empty proofs.Fill empty proofs.Unify constructor naming scheme.WIP...Add {,pre}image_any, try inductive versions.Mv sum_pn_linear to sum_n.v.sum_n needs new alias LM = ../LM.sum_n now need alias LM = ../LM.More abstract statement for sum_pn_linear (same proof).Try this.WIP: unify any(P)/finite/seq.