{"header":{"message":"First commit. Definition of the axioms, some basic infinitesimal spaces, and a few basic concepts. Some theorems have been left unproven.","description":null,"timestamp":"2022-02-19T22:26:57.472167916Z","authors":[{}]},"hash":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC","authors":[{"login":"finegeometer","key":"64ARLu9ao3fdRKWR644xoCX9eBBEMzfkyWsK7kYdkcxn"}],"deps":{"hashes":[["52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC","First commit. Definition of the axioms, some basic infinitesimal spaces, and a few basic concepts. Some theorems have been left unproven."],["AA",null],["AQCD6V5YNXT7KATO2KVAFOXXPTTYARJ55GNNKEHVQKDA7MUIANBAC",""]],"deps":["AQCD6V5YNXT7KATO2KVAFOXXPTTYARJ55GNNKEHVQKDA7MUIANBAC"],"known":[]},"hunks":[{"FileAdd":{"meta":{"basename":"theories","metadata":576},"context":[{"change":2,"pos":1}],"contents":[]}},{"FileAdd":{"meta":{"basename":"weil_algebras.v","metadata":0},"context":[{"change":0,"pos":20}],"contents":[{"Add":{"text":"From Coq Require Import FunctionalExtensionality ProofIrrelevance.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:129"}},{"Add":{"text":"From mathcomp Require Import all_ssreflect ssralg.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:180"}},{"Add":{"text":"Require Import isomorphism.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:208"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:209"}},{"Add":{"text":"Open Scope R.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:223"}},{"Add":{"text":"Import GRing.Theory.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:244"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:245"}},{"Add":{"text":"Section WeilAlgebras.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:267"}},{"Add":{"text":"Variables (R : comRingType).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:296"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:297"}},{"Add":{"text":"Record WeilData : Type := {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:325"}},{"Add":{"text":" Domain : finType;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:347"}},{"Add":{"text":" Mul : {ffun Domain -> R^o} -> {ffun Domain -> R^o} -> {ffun Domain -> R^o};","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:427"}},{"Add":{"text":" Lin : forall a, linear (Mul a);","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:463"}},{"Add":{"text":" Assoc : associative Mul;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:492"}},{"Add":{"text":" Comm : commutative Mul;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:520"}},{"Add":{"text":" Nilpotent : exists T : finType,","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:556"}},{"Add":{"text":" forall (x : {ffun Domain -> R}) (xs : T -> {ffun Domain -> R}),","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:628"}},{"Add":{"text":" \\big[Mul/x]_(i : T) (xs i) = 0","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:667"}},{"Add":{"text":"}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:670"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:671"}},{"Add":{"text":"Section WeilImpls.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:690"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:691"}},{"Add":{"text":" Variables (W : WeilData).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:721"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:722"}},{"Add":{"text":" Definition weil : Type := R * {ffun (Domain W) -> R^o}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:782"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:783"}},{"Add":{"text":" Definition wrap (w : R * {ffun Domain W -> R}) : weil := w.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:847"}},{"Add":{"text":" Definition unwrap (w : weil) : R * {ffun Domain W -> R} := w.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:913"}},{"Add":{"text":" Lemma wrap_unwrap : cancel wrap unwrap.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:957"}},{"Add":{"text":" move=> w. by rewrite /wrap /unwrap.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1001"}},{"Add":{"text":" Qed.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1010"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1011"}},{"Add":{"text":" Canonical weil_eq : eqType := EqType weil (CanEqMixin wrap_unwrap).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1083"}},{"Add":{"text":" Canonical weil_choice : choiceType := ChoiceType weil (CanChoiceMixin wrap_unwrap).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1171"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1172"}},{"Add":{"text":" Canonical weil_zmodType : zmodType :=","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1214"}},{"Add":{"text":" ZmodType weil (ZmodMixin (@addrA _) (@addrC _) (@add0r _) (@addNr _)).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1293"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1294"}},{"Add":{"text":" Definition weil_mul (x y : weil) : weil :=","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1341"}},{"Add":{"text":" ( fst x * fst y","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1365"}},{"Add":{"text":" , fst x *: snd y + fst y *: snd x + Mul W (snd x) (snd y)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1431"}},{"Add":{"text":" ).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1442"}},{"Add":{"text":" Definition weil_one : weil := ( 1 , [ffun=> 0]).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1495"}},{"Add":{"text":" Fact weil_mulA : associative weil_mul.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1538"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1552"}},{"Add":{"text":" Fact weil_mulC : commutative weil_mul.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1595"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1609"}},{"Add":{"text":" Fact weil_mul_1l : left_id weil_one weil_mul.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1659"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1673"}},{"Add":{"text":" Fact weil_mul_1r : right_id weil_one weil_mul.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1724"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1738"}},{"Add":{"text":" Fact weil_mul_addl : left_distributive weil_mul +%R.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1795"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1809"}},{"Add":{"text":" Fact weil_mul_addr : right_distributive weil_mul +%R.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1867"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1881"}},{"Add":{"text":" Fact weil1_nonzero : weil_one != 0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1921"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1935"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1936"}},{"Add":{"text":" Canonical weil_ringType : ringType := RingType weil ","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:1993"}},{"Add":{"text":" (RingMixin weil_mulA weil_mul_1l weil_mul_1r weil_mul_addl weil_mul_addr weil1_nonzero).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2090"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2091"}},{"Add":{"text":" Canonical weil_comRingType : comRingType := ComRingType weil weil_mulC.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2167"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2168"}},{"Add":{"text":" Definition weil_scale (k : R) (w : weil) : weil","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2220"}},{"Add":{"text":" := (k * fst w, [ffun a => k *: snd w a]).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2270"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2271"}},{"Add":{"text":" Fact weil_scaleA k1 k2 f :","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2302"}},{"Add":{"text":" weil_scale k1 (weil_scale k2 f) = weil_scale (k1 * k2) f.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2364"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2378"}},{"Add":{"text":" Fact weil_scale1 : left_id 1 weil_scale.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2423"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2437"}},{"Add":{"text":" Fact weil_scale_addr k : {morph (weil_scale k) : x y / x + y}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2504"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2518"}},{"Add":{"text":" Fact weil_scale_addl u : {morph (weil_scale)^~ u : k1 k2 / k1 + k2}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2591"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2605"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2606"}},{"Add":{"text":" Canonical weil_lmodType : lmodType R := ","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2651"}},{"Add":{"text":" LmodType R weil (LmodMixin weil_scaleA weil_scale1 weil_scale_addr weil_scale_addl).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2744"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2745"}},{"Add":{"text":" Fact weil_scaleAl (a : R) (u v : weil) : a *: (u * v) = (a *: u) * v.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2819"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2833"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2834"}},{"Add":{"text":" Fact weil_scaleAr (a : R) (u v : weil) : a *: (u * v) = u * (a *: v).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2908"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2922"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2923"}},{"Add":{"text":" Canonical weil_lalgType : lalgType R := LalgType R weil weil_scaleAl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:2997"}},{"Add":{"text":" Canonical weil_algType : algType R := AlgType R weil weil_scaleAr.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3068"}},{"Add":{"text":" Canonical weil_comAlgType : comAlgType R := [comAlgType R of weil].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3140"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3141"}},{"Add":{"text":"End WeilImpls.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3156"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3157"}},{"Add":{"text":"End WeilAlgebras.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3175"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3176"}},{"Add":{"text":"Definition Weil {R} W := weil_comAlgType R W.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3222"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3223"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3224"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3225"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3226"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3227"}},{"Add":{"text":"Definition WeilMorph {R} (W : WeilData R) (A : algType R) : Type :=","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3295"}},{"Add":{"text":" {f : {ffun (Domain R W) -> A} ","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3330"}},{"Add":{"text":" | {morph (fun (x : {ffun _ -> R^o}) => \\sum_(i : Domain R W) (x i *: f i)) ","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3410"}},{"Add":{"text":" : x y / Mul R W x y >-> x * y","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3448"}},{"Add":{"text":" }}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3456"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3457"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3458"}},{"Add":{"text":"Module Export IsoImpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3481"}},{"Add":{"text":"(* The proofs below are a mess, but they work. *)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3531"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3532"}},{"Add":{"text":"Section reify.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3547"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3548"}},{"Add":{"text":" Context {R} {W : WeilData R} {A : algType R} (m : WeilMorph W A).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3618"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3619"}},{"Add":{"text":" Definition reify : Weil W -> A :=","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3657"}},{"Add":{"text":" let '(exist dom_f morph) := m in","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3698"}},{"Add":{"text":" fun '(x, dx) => x%:A + (\\sum_i dx i *: dom_f i).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3755"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3756"}},{"Add":{"text":" Fact reify_is_additive : additive reify.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3801"}},{"Add":{"text":" Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3812"}},{"Add":{"text":" rewrite /reify; move: m => [dom_f morph].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3862"}},{"Add":{"text":" move=> [x dx] [y dy]. simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3899"}},{"Add":{"text":" rewrite scalerDl -addrA -addrA; f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:3948"}},{"Add":{"text":" rewrite opprD addrA [_ - y%:A]addrC -addrA scaleNr; f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4017"}},{"Add":{"text":" rewrite -sumrB.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4041"}},{"Add":{"text":" apply: eq_bigr => i _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4072"}},{"Add":{"text":" rewrite -scaleNr -scalerDl; f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4117"}},{"Add":{"text":" by rewrite {1}/+%R {1}/-%R; simpl; rewrite /ffun_add /ffun_opp ffunE ffunE.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4201"}},{"Add":{"text":" Qed.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4210"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4211"}},{"Add":{"text":" Canonical reify_additive := Additive reify_is_additive.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4271"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4272"}},{"Add":{"text":" Fact reify_is_multiplicative : multiplicative reify.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4329"}},{"Add":{"text":" Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4340"}},{"Add":{"text":" rewrite /reify; move: m => [dom_f morph].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4390"}},{"Add":{"text":" split.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4405"}},{"Add":{"text":" - move=> [x dx] [y dy]. simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4444"}},{"Add":{"text":" rewrite mulrDr mulrDl mulrDl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4486"}},{"Add":{"text":" rewrite -morph.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4514"}},{"Add":{"text":" rewrite -[x%:A*_+_+_]addrA -scalerAl -scalerAr scalerA mulr1; f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4597"}},{"Add":{"text":" rewrite mulr_suml mulr_sumr -big_split -big_split; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4667"}},{"Add":{"text":" apply: eq_bigr => i _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4702"}},{"Add":{"text":" rewrite -scalerAr mulr1 scalerA.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4747"}},{"Add":{"text":" rewrite -scalerAl mul1r scalerA.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4792"}},{"Add":{"text":" rewrite -scalerDl -scalerDl addrA; f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4848"}},{"Add":{"text":" rewrite {1 2}/+%R {1 2}/*:%R; simpl; rewrite /ffun_add /ffun_scale.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4928"}},{"Add":{"text":" do 4 rewrite ffunE; f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:4969"}},{"Add":{"text":" by rewrite addrC /*:%R; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5012"}},{"Add":{"text":" - simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5029"}},{"Add":{"text":" rewrite big1.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5055"}},{"Add":{"text":" + by rewrite addr0 scale1r.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5095"}},{"Add":{"text":" + by move=> i _; rewrite ffunE scale0r.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5147"}},{"Add":{"text":" Qed.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5156"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5157"}},{"Add":{"text":" Canonical reify_multiplicative := AddRMorphism reify_is_multiplicative.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5233"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5234"}},{"Add":{"text":" Fact reify_is_scalable : scalable reify.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5279"}},{"Add":{"text":" Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5290"}},{"Add":{"text":" rewrite /reify; move: m => [dom_f morph].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5340"}},{"Add":{"text":" move=> k [x dx]. simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5372"}},{"Add":{"text":" rewrite scalerDr scalerA; f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5415"}},{"Add":{"text":" rewrite scaler_sumr.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5444"}},{"Add":{"text":" apply: eq_bigr => i _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5475"}},{"Add":{"text":" by rewrite ffunE scalerA.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5509"}},{"Add":{"text":" Qed.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5518"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5519"}},{"Add":{"text":" Canonical reify_linear := AddLinear reify_is_scalable.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5578"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5579"}},{"Add":{"text":" Definition LR_of_WeilMorph : {lrmorphism (Weil W) -> A}","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5639"}},{"Add":{"text":" := [lrmorphism of reify].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5673"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5674"}},{"Add":{"text":"End reify.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5685"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5686"}},{"Add":{"text":"Definition unreify {R} {W : WeilData R} {A : algType R}","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5742"}},{"Add":{"text":" (f : {lrmorphism (Weil W) -> A}) : {ffun Domain R W -> A}","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5804"}},{"Add":{"text":" := [ffun i => f (0, [ffun j => if i == j then 1 else 0])].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5867"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5868"}},{"Add":{"text":"Lemma unreify_morph {R} {W : WeilData R} {A : algType R}","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5925"}},{"Add":{"text":" (f : {lrmorphism (Weil W) -> A}) :","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5964"}},{"Add":{"text":" { morph ","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:5977"}},{"Add":{"text":" (fun x : {ffun Domain R W -> R^o} => \\sum_i x i *: (unreify f) i) ","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6052"}},{"Add":{"text":" : x y / Mul R W x y >-> x * y","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6090"}},{"Add":{"text":" }.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6097"}},{"Add":{"text":"Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6104"}},{"Add":{"text":" move=> x y.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6120"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6121"}},{"Add":{"text":" have: forall (g : Domain R W -> R^o), ","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6164"}},{"Add":{"text":" (\\sum_i g i *: (unreify f) i) = f (0, [ffun i => g i]).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6228"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6234"}},{"Add":{"text":" move=> g.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6252"}},{"Add":{"text":" have: \\sum_i g i *: (unreify f) i = \\sum_i f (0, [ffun j => if i == j then g i else 0]).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6349"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6359"}},{"Add":{"text":" apply: eq_bigr => i _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6394"}},{"Add":{"text":" rewrite /(unreify f) ffunE -linearZ_LR.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6446"}},{"Add":{"text":" rewrite /*:%R; simpl; rewrite /weil_scale; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6508"}},{"Add":{"text":" rewrite mulr0; f_equal; f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6553"}},{"Add":{"text":" apply: eq_ffun => j.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6586"}},{"Add":{"text":" rewrite ffunE.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6613"}},{"Add":{"text":" case: (i == j).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6641"}},{"Add":{"text":" + by rewrite /*:%R; simpl; rewrite mulr1.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6695"}},{"Add":{"text":" + by rewrite scaler0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6729"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6739"}},{"Add":{"text":" move=>->.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6757"}},{"Add":{"text":" rewrite -linear_sum.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6786"}},{"Add":{"text":" apply: f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6810"}},{"Add":{"text":" have: \\sum_i (0, [ffun j => if i == j then g i else 0])","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6874"}},{"Add":{"text":" = (0, \\sum_i [ffun j => if i == j then g i else 0]).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6939"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6949"}},{"Add":{"text":" move=> t.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:6971"}},{"Add":{"text":" elim/big_rec2 : _ => // [i da [b db] _ ->].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7027"}},{"Add":{"text":" rewrite /+%R; simpl; rewrite /add_pair /ffun_add; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7096"}},{"Add":{"text":" rewrite addr0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7123"}},{"Add":{"text":" done.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7141"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7151"}},{"Add":{"text":" move=>->.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7169"}},{"Add":{"text":" f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7186"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7187"}},{"Add":{"text":" rewrite -ffunP => i.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7216"}},{"Add":{"text":" rewrite ffunE sum_ffunE.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7249"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7250"}},{"Add":{"text":" have: \\sum_k [ffun j => if k == j then g k else 0] i","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7311"}},{"Add":{"text":" = \\sum_k if k == i then g k else 0","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7358"}},{"Add":{"text":" by apply: eq_bigr => k _; rewrite ffunE.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7411"}},{"Add":{"text":" move=>->.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7429"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7430"}},{"Add":{"text":" rewrite -big_mkcond; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7466"}},{"Add":{"text":" by rewrite big_pred1_eq.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7499"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7505"}},{"Add":{"text":" move=> lemma; rewrite lemma lemma lemma; clear lemma.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7563"}},{"Add":{"text":" rewrite -rmorphM.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7585"}},{"Add":{"text":" rewrite /*%R; simpl; rewrite /weil_mul; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7636"}},{"Add":{"text":" rewrite mul0r scale0r scale0r add0r add0r.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7683"}},{"Add":{"text":" f_equal; f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7705"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7706"}},{"Add":{"text":" have: forall (g : {ffun Domain R W -> R^o}), [ffun i => g i] = g.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7776"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7782"}},{"Add":{"text":" move=> g.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7800"}},{"Add":{"text":" apply ffunP => i.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7826"}},{"Add":{"text":" by rewrite ffunE.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7852"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7858"}},{"Add":{"text":" by move=> lemma; rewrite lemma lemma lemma; clear lemma.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7919"}},{"Add":{"text":"Qed.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7924"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7925"}},{"Add":{"text":"Definition WeilMorph_of_LR {R} {W : WeilData R} {A : algType R}","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:7989"}},{"Add":{"text":" (f : {lrmorphism (Weil W) -> A}) : WeilMorph W A","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8042"}},{"Add":{"text":" := exist _ (unreify f) (unreify_morph f).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8088"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8089"}},{"Add":{"text":"Theorem LR_W_LR {R} {W : WeilData R} {A : algType R}","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8142"}},{"Add":{"text":" : cancel WeilMorph_of_LR (@LR_of_WeilMorph R W A).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8197"}},{"Add":{"text":" move=> m.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8211"}},{"Add":{"text":" have: forall w, LR_of_WeilMorph (WeilMorph_of_LR m) w = m w.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8276"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8282"}},{"Add":{"text":" move=> [x dx]. simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8312"}},{"Add":{"text":" rewrite /unreify.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8338"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8339"}},{"Add":{"text":" have: \\sum_i dx i *: [ffun i0 => m (0, [ffun j => if i0 == j then 1 else 0])] i","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8427"}},{"Add":{"text":" = \\sum_i m (0, dx i *: [ffun j => if i == j then 1 else 0]).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8500"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8510"}},{"Add":{"text":" apply: eq_bigr => i _; rewrite ffunE -linearZ_LR.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8572"}},{"Add":{"text":" rewrite {3}/*:%R; simpl; rewrite /weil_scale; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8637"}},{"Add":{"text":" rewrite mulr0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8664"}},{"Add":{"text":" f_equal; f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8694"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8704"}},{"Add":{"text":" move=>->.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8722"}},{"Add":{"text":" rewrite -linear_sum.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8751"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8752"}},{"Add":{"text":" have: \\sum_i (0, dx i *: [ffun j => if i == j then 1 : R^o else 0])","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8828"}},{"Add":{"text":" = (0, \\sum_i dx i *: [ffun j => if i == j then 1 : R^o else 0]).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8905"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8915"}},{"Add":{"text":" move=> t.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8937"}},{"Add":{"text":" elim/big_rec2 : _ => // [i da [b db] _ ->].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:8993"}},{"Add":{"text":" rewrite /+%R; simpl; rewrite /add_pair /ffun_add; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9062"}},{"Add":{"text":" rewrite addr0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9089"}},{"Add":{"text":" done.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9107"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9117"}},{"Add":{"text":" move=>->.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9135"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9136"}},{"Add":{"text":" have: x%:A = m (x%:A) by rewrite linearZ_LR rmorph1.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9197"}},{"Add":{"text":" move=>->.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9215"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9216"}},{"Add":{"text":" rewrite -linearD.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9242"}},{"Add":{"text":" rewrite {3}/*:%R; simpl; rewrite /weil_scale; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9303"}},{"Add":{"text":" apply: f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9327"}},{"Add":{"text":" rewrite pair_equal_spec; split; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9374"}},{"Add":{"text":" - by rewrite addr0 mulr1.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9408"}},{"Add":{"text":" - rewrite -ffunP => i.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9439"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9440"}},{"Add":{"text":" rewrite ffunE ffunE ffunE.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9479"}},{"Add":{"text":" rewrite scaler0 add0r sum_ffunE.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9524"}},{"Add":{"text":" have: \\sum_k (dx k *: [ffun j => if k == j then 1 : R^o else 0]) i","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9603"}},{"Add":{"text":" = \\sum_k (if k == i then dx k else 0).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9658"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9672"}},{"Add":{"text":" apply: eq_bigr => k _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9711"}},{"Add":{"text":" rewrite /*:%R; simpl; rewrite /ffun_scale ffunE ffunE.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9782"}},{"Add":{"text":" rewrite /*:%R; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9820"}},{"Add":{"text":" case: (k == i).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9852"}},{"Add":{"text":" - by rewrite mulr1.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9888"}},{"Add":{"text":" - by rewrite mulr0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9924"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9938"}},{"Add":{"text":" move=>->.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9960"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:9961"}},{"Add":{"text":" rewrite -big_mkcond; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10001"}},{"Add":{"text":" by rewrite big_pred1_eq.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10038"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10044"}},{"Add":{"text":" move /functional_extensionality.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10081"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10082"}},{"Add":{"text":" case: (LR_of_WeilMorph (WeilMorph_of_LR m)) => f1 pf1.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10141"}},{"Add":{"text":" case: m => f2 pf2.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10164"}},{"Add":{"text":" simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10175"}},{"Add":{"text":" move=> eq; move: eq pf1 pf2 => -> pf1 pf2.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10222"}},{"Add":{"text":" by move: (proof_irrelevance _ pf1 pf2) => ->.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10272"}},{"Add":{"text":"Qed.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10277"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10278"}},{"Add":{"text":"Theorem W_LR_W {R} {W : WeilData R} {A : algType R}","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10330"}},{"Add":{"text":" : cancel (@LR_of_WeilMorph R W A) WeilMorph_of_LR.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10385"}},{"Add":{"text":" move=> [dom_f morph].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10411"}},{"Add":{"text":" apply: eq_sig; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10437"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10443"}},{"Add":{"text":" rewrite /unreify; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10476"}},{"Add":{"text":" rewrite -ffunP => i.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10505"}},{"Add":{"text":" rewrite ffunE.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10528"}},{"Add":{"text":" rewrite scale0r add0r .","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10560"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10561"}},{"Add":{"text":" have: \\sum_k [ffun j => if i == j then 1 else 0] k *: dom_f k","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10631"}},{"Add":{"text":" = \\sum_k if k == i then dom_f k else 0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10683"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10693"}},{"Add":{"text":" apply: eq_bigr => k _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10728"}},{"Add":{"text":" rewrite ffunE.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10755"}},{"Add":{"text":" rewrite eq_sym.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10783"}},{"Add":{"text":" case: (k == i).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10811"}},{"Add":{"text":" - by rewrite scale1r.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10845"}},{"Add":{"text":" - by rewrite scale0r.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10879"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10889"}},{"Add":{"text":" move=>->.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10907"}},{"Add":{"text":" rewrite -big_mkcond; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10943"}},{"Add":{"text":" by rewrite big_pred1_eq.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10976"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10982"}},{"Add":{"text":" move=> H.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:10996"}},{"Add":{"text":" apply proof_irrelevance.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11025"}},{"Add":{"text":"Qed.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11030"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11031"}},{"Add":{"text":"Definition reifyIso {R} {W : WeilData R} {A : algType R} :","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11090"}},{"Add":{"text":" WeilMorph W A <--> {lrmorphism Weil W -> A} := {|","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11144"}},{"Add":{"text":" Forward := LR_of_WeilMorph;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11176"}},{"Add":{"text":" Backward := WeilMorph_of_LR;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11209"}},{"Add":{"text":" BF := W_LR_W;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11227"}},{"Add":{"text":" FB := LR_W_LR;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11246"}},{"Add":{"text":"|}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11250"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11251"}},{"Add":{"text":"End IsoImpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11264"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11265"}}]}},{"FileAdd":{"meta":{"basename":"isomorphism.v","metadata":0},"context":[{"change":0,"pos":20}],"contents":[{"Add":{"text":"From Coq Require Import ssreflect ssrfun FunctionalExtensionality.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11372"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11373"}},{"Add":{"text":"Record Isomorphism (A B : Type) := {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11410"}},{"Add":{"text":" Forward : A -> B;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11432"}},{"Add":{"text":" Backward : B -> A;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11455"}},{"Add":{"text":" BF : cancel Forward Backward;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11489"}},{"Add":{"text":" FB : cancel Backward Forward;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11523"}},{"Add":{"text":"}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11526"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11527"}},{"Add":{"text":"Infix \"<-->\" := Isomorphism (at level 95, no associativity).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11588"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11589"}},{"Add":{"text":"Definition iso_refl {A : Type} : A <--> A := {|","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11637"}},{"Add":{"text":" Forward x := x;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11657"}},{"Add":{"text":" Backward x := x;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11678"}},{"Add":{"text":" BF x := eq_refl;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11699"}},{"Add":{"text":" FB x := eq_refl;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11720"}},{"Add":{"text":"|}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11724"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11725"}},{"Add":{"text":"Definition iso_sym {A B : Type} (α : A <--> B) : B <--> A := {|","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11790"}},{"Add":{"text":" Forward x := Backward _ _ α x;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11826"}},{"Add":{"text":" Backward x := Forward _ _ α x;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11862"}},{"Add":{"text":" BF x := FB _ _ α x;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11887"}},{"Add":{"text":" FB x := BF _ _ α x;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11912"}},{"Add":{"text":"|}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11916"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11917"}},{"Add":{"text":"Definition iso_trans {A B C : Type} (α : A <--> B) (β : B <--> C) : A <--> C.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:11997"}},{"Add":{"text":"Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12004"}},{"Add":{"text":" refine ({|","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12019"}},{"Add":{"text":" Forward x := Forward _ _ β (Forward _ _ α x);","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12075"}},{"Add":{"text":" Backward x := Backward _ _ α (Backward _ _ β x);","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12134"}},{"Add":{"text":" BF x := _;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12153"}},{"Add":{"text":" FB x := _;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12172"}},{"Add":{"text":" |}).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12181"}},{"Add":{"text":" - by rewrite BF BF.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12205"}},{"Add":{"text":" - by rewrite FB FB.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12229"}},{"Add":{"text":"Qed.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12234"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12235"}},{"Add":{"text":"Definition iso_exp {A B C : Type} (α : A <--> B) : (A -> C) <--> (B -> C).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12311"}},{"Add":{"text":"Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12318"}},{"Add":{"text":" refine ({|","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12333"}},{"Add":{"text":" Forward f x := f (Backward _ _ α x);","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12379"}},{"Add":{"text":" Backward f x := f (Forward _ _ α x);","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12425"}},{"Add":{"text":" BF f := _;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12444"}},{"Add":{"text":" FB f := _;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12463"}},{"Add":{"text":" |}).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12472"}},{"Add":{"text":" - apply functional_extensionality => x.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12516"}},{"Add":{"text":" by rewrite BF.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12539"}},{"Add":{"text":" - apply functional_extensionality => x.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12583"}},{"Add":{"text":" by rewrite FB.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12606"}},{"Add":{"text":"Qed.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12611"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12612"}}]}},{"FileAdd":{"meta":{"basename":"common.v","metadata":0},"context":[{"change":0,"pos":20}],"contents":[{"Add":{"text":"(* https://math.stackexchange.com/questions/3802938/computational-type-theory-for-topos-logic *)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12744"}},{"Add":{"text":"From mathcomp Require Export all_ssreflect ssralg.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12795"}},{"Add":{"text":"Require Export isomorphism atomic weil_algebras axioms basic_infinitesimal_spaces.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12878"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12879"}},{"Add":{"text":"Definition fiber {E B} (f : E -> B) : B -> Type","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12927"}},{"Add":{"text":" := fun b => {e : E | f e = b}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12962"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:12963"}},{"Add":{"text":"Definition bundle {B} (f : B -> Type) : Type","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13008"}},{"Add":{"text":" := {b : B & f b}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13030"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13031"}},{"Add":{"text":"Definition field {B} (f : B -> Type) : Type","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13075"}},{"Add":{"text":" := forall b : B, f b.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13101"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13102"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13103"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13104"}},{"Add":{"text":"Lemma bundle_fiber {E B} (f : E -> B) : bundle (fiber f) <--> E.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13169"}},{"Add":{"text":"Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13176"}},{"Add":{"text":" refine({|","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13190"}},{"Add":{"text":" Forward '(existT b (exist e _)) := e;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13236"}},{"Add":{"text":" Backward e := existT _ (f e) (exist _ e erefl);","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13292"}},{"Add":{"text":" |}).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13301"}},{"Add":{"text":" - move=> [b [e pf]].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13326"}},{"Add":{"text":" move: b pf.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13346"}},{"Add":{"text":" by apply: eq_indd.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13373"}},{"Add":{"text":" - done.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13385"}},{"Add":{"text":"Defined.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13394"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13395"}},{"Add":{"text":"Lemma fiber_bundle {B} {F : B -> Type} {b} ","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13439"}},{"Add":{"text":" : fiber (projT1 (P := _) : bundle F -> B) b <--> F b.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13497"}},{"Add":{"text":"Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13504"}},{"Add":{"text":" refine({|","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13518"}},{"Add":{"text":" Forward '(exist (existT x f) pf) := eq_rect _ F f _ pf;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13582"}},{"Add":{"text":" Backward f := exist _ (existT _ b f) erefl;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13634"}},{"Add":{"text":" |}).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13643"}},{"Add":{"text":" - move=> [[b' f] pf].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13669"}},{"Add":{"text":" move: b pf.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13689"}},{"Add":{"text":" by apply: eq_indd.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13716"}},{"Add":{"text":" - done.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13728"}},{"Add":{"text":"Defined.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13737"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13738"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13739"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13740"}},{"Add":{"text":"Definition tangent_bundle M := 'D_1 -> M.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13782"}},{"Add":{"text":"Definition tangent M := fiber (fun f : tangent_bundle M => f zero).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13850"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13851"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13852"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13853"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13854"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13855"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13856"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13857"}}]}},{"FileAdd":{"meta":{"basename":"basic_infinitesimal_spaces.v","metadata":0},"context":[{"change":0,"pos":20}],"contents":[{"Add":{"text":"From mathcomp Require Import all_ssreflect ssralg.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:13963"}},{"Add":{"text":"Require Import isomorphism axioms atomic.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14005"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14006"}},{"Add":{"text":"Class Zero T := { zero : T }.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14036"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14037"}},{"Add":{"text":"(* The nth-order infinitesimals. *)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14073"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14074"}},{"Add":{"text":"Definition nilpotent n := {x : R | x ^+ n = 0}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14122"}},{"Add":{"text":"Definition nilpotent_union := {x : R | exists n, x ^+ n = 0}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14184"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14185"}},{"Add":{"text":"Notation \"''D_' n\" := (nilpotent (n.+1))","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14226"}},{"Add":{"text":" (at level 8, n at level 2, format \"''D_' n\").","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14276"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14277"}},{"Add":{"text":"Notation \"''D_-1'\" := (nilpotent 0)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14313"}},{"Add":{"text":" (at level 8, format \"''D_-1'\").","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14349"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14350"}},{"Add":{"text":"Notation \"''D_∞'\" := nilpotent_union","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14389"}},{"Add":{"text":" (at level 8, format \"''D_∞'\").","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14426"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14427"}},{"Add":{"text":"Coercion R_of_nilpotent_union (d : nilpotent_union) : R := proj1_sig d.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14499"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14500"}},{"Add":{"text":"Coercion union_of_nilpotent {n} : nilpotent n -> 'D_∞.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14557"}},{"Add":{"text":" move=> [x pf].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14576"}},{"Add":{"text":" exists x.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14590"}},{"Add":{"text":" exists n.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14604"}},{"Add":{"text":" exact pf.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14618"}},{"Add":{"text":"Defined.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14627"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14628"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14629"}},{"Add":{"text":"Fact higher_power_still_zero {x : R} {m n} (leq : m <= n)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14687"}},{"Add":{"text":" : x ^+ m = 0 -> x ^+ n = 0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14719"}},{"Add":{"text":"Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14726"}},{"Add":{"text":" rewrite -(subnK leq) exprD => ->.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14764"}},{"Add":{"text":" apply: mulr0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14782"}},{"Add":{"text":"Qed.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14787"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14788"}},{"Add":{"text":"Definition widen_nilpotent {m n} (leq : m <= n) : nilpotent m -> nilpotent n := ","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14869"}},{"Add":{"text":" fun '(exist x pf) => (exist _ x (higher_power_still_zero leq pf)).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14940"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14941"}},{"Add":{"text":"#[refine]","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14951"}},{"Add":{"text":"Global Instance D_zero {n} : Zero 'D_n := {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:14995"}},{"Add":{"text":" zero := exist _ 0 _","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15019"}},{"Add":{"text":"}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15022"}},{"Add":{"text":"apply: expr0n.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15037"}},{"Add":{"text":"Defined.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15046"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15047"}},{"Add":{"text":"Global Instance nilpotent_union_zero : Zero nilpotent_union := {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15112"}},{"Add":{"text":" zero := (zero : 'D_0)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15138"}},{"Add":{"text":"}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15141"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15142"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15143"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15144"}},{"Add":{"text":"Definition d_minus_void_iso : 'D_-1 <--> void.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15191"}},{"Add":{"text":"Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15198"}},{"Add":{"text":" have: 'D_-1 -> void.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15223"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15229"}},{"Add":{"text":" move=>[x pf].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15251"}},{"Add":{"text":" rewrite expr0 in pf.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15280"}},{"Add":{"text":" move: (oner_neq0 R).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15309"}},{"Add":{"text":" by move /eqP.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15331"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15337"}},{"Add":{"text":" move=> fwd.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15353"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15354"}},{"Add":{"text":" refine ({|","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15369"}},{"Add":{"text":" Forward := fwd;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15393"}},{"Add":{"text":" Backward := of_void _;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15424"}},{"Add":{"text":" BF x := match fwd x with end;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15462"}},{"Add":{"text":" FB x := match x with end;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15496"}},{"Add":{"text":" |}).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15505"}},{"Add":{"text":"Defined.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15514"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15515"}},{"Add":{"text":"Definition polynomial {n} (coeffs : 'I_n -> R) (x : R) : R","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15574"}},{"Add":{"text":" := \\prod_(i < n) ((x ^+ i) * coeffs i).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15618"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15619"}},{"Add":{"text":"(* Implementation at the bottom of the file. *)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15667"}},{"Add":{"text":"Module Type nilpotent_properties_sig.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15705"}},{"Add":{"text":" Axiom KL_D : forall {n}, (nilpotent n -> R) <--> ('I_n -> R).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15771"}},{"Add":{"text":" Axiom KL_D_back : forall {n coeffs} {d : nilpotent n},","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15830"}},{"Add":{"text":" Backward _ _ KL_D coeffs d = polynomial coeffs d.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15888"}},{"Add":{"text":" Axiom atomicD : forall {n}, Atomic 'D_n.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15933"}},{"Add":{"text":"End nilpotent_properties_sig.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15963"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15964"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15965"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15966"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15967"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15968"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15969"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15970"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15971"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15972"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:15973"}},{"Add":{"text":"(* Spaces of infinitesimal vectors. *)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16012"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16013"}},{"Add":{"text":"(* I think this space acts like a walking simplex? *)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16067"}},{"Add":{"text":"Definition Δ n := {x : 'I_n -> R | forall i j, x i * x j = 0}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16131"}},{"Add":{"text":"Coercion Rn_of_Δ {n} (d : Δ n) : {ffun 'I_n -> R} := finfun (proj1_sig d).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16208"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16209"}},{"Add":{"text":"#[refine]","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16219"}},{"Add":{"text":"Global Instance Δ_zero {n} : Zero (Δ n) := {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16266"}},{"Add":{"text":" zero := exist _ (fun=> 0) (fun _ _ => _)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16311"}},{"Add":{"text":"}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16314"}},{"Add":{"text":"exact (mul0r 0).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16331"}},{"Add":{"text":"Defined.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16340"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16341"}},{"Add":{"text":"Lemma eq_Δ {n} {u v : Δ n} (pf : forall i, u i = v i) : u = v.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16406"}},{"Add":{"text":" move: u v pf => [u pf_u] [v pf_v] pf.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16448"}},{"Add":{"text":" rewrite /Rn_of_Δ in pf; simpl in pf.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16490"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16491"}},{"Add":{"text":" have: u = v.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16508"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16514"}},{"Add":{"text":" apply: functional_extensionality => i.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16561"}},{"Add":{"text":" move: (pf i).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16583"}},{"Add":{"text":" by rewrite ffunE ffunE.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16615"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16621"}},{"Add":{"text":" move=> tmp. move: tmp pf_v pf => <- pf_v _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16669"}},{"Add":{"text":" f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16682"}},{"Add":{"text":" apply: proof_irrelevance.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16712"}},{"Add":{"text":"Qed.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16717"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16718"}},{"Add":{"text":"Definition Δ1_D_iso_fwd : Δ 1 -> 'D_1 :=","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16761"}},{"Add":{"text":" fun '(exist x pf) => ","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16787"}},{"Add":{"text":" exist _ (x ord0) (Logic.eq_trans (expr2 (x ord0)) (pf ord0 ord0)).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16862"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16863"}},{"Add":{"text":"Definition Δ1_D_iso_bwd : 'D_1 -> Δ 1.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16904"}},{"Add":{"text":" refine(fun '(exist x pf) => exist _ (fun=> x) _).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16958"}},{"Add":{"text":" by rewrite -expr2 pf.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16984"}},{"Add":{"text":"Defined.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16993"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:16994"}},{"Add":{"text":"Definition Δ1_D_iso : Δ 1 <--> 'D_1.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17033"}},{"Add":{"text":"Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17040"}},{"Add":{"text":" refine ({|","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17055"}},{"Add":{"text":" Forward := Δ1_D_iso_fwd;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17089"}},{"Add":{"text":" Backward := Δ1_D_iso_bwd;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17124"}},{"Add":{"text":" |}).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17133"}},{"Add":{"text":" - move=> [x pf].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17154"}},{"Add":{"text":" apply: eq_Δ => i.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17181"}},{"Add":{"text":" rewrite /Rn_of_Δ ffunE ffunE; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17227"}},{"Add":{"text":" by rewrite ord1.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17252"}},{"Add":{"text":" - move=> [x pf]; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17280"}},{"Add":{"text":" f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17297"}},{"Add":{"text":" apply: proof_irrelevance.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17331"}},{"Add":{"text":"Defined.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17340"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17341"}},{"Add":{"text":"(* Implementation at the bottom of the file. *)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17389"}},{"Add":{"text":"Module Type Δ_properties_sig.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17420"}},{"Add":{"text":" Axiom KL_Δ : forall {n}, (Δ n -> R) <--> (R * ('I_n -> R)).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17486"}},{"Add":{"text":" Axiom KL_Δ_back : forall {n coeffs} {d : Δ n},","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17539"}},{"Add":{"text":" Backward _ _ KL_Δ coeffs d = fst coeffs + \\sum_i snd coeffs i * d i.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17617"}},{"Add":{"text":" Axiom atomicΔ : forall {n}, Atomic (Δ n).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17665"}},{"Add":{"text":"End Δ_properties_sig.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17688"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17689"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17690"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17691"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17692"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17693"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17694"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17695"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17696"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17697"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17698"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17699"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17700"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17701"}},{"Add":{"text":"(* Implementation details that involve Weil algebras *)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17757"}},{"Add":{"text":"Require Import weil_algebras.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17787"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17788"}},{"Add":{"text":"Module Export nilpotent_properties : nilpotent_properties_sig.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17851"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17852"}},{"Add":{"text":" Definition nilpotent_weil_mul n","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17888"}},{"Add":{"text":" (x : {ffun 'I_n -> R^o}) (y : {ffun 'I_n -> R^o}) : {ffun 'I_n -> R^o} :=","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:17966"}},{"Add":{"text":" [ffun k : 'I_n => \\sum_(i < n) \\sum_(j < n) ","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18015"}},{"Add":{"text":" if (i + j + 1 == k)%N then x i * y j else 0","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18067"}},{"Add":{"text":" ].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18074"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18075"}},{"Add":{"text":" Fact nilpotent_weil_mul_linear n z : linear (nilpotent_weil_mul n z).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18149"}},{"Add":{"text":" Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18160"}},{"Add":{"text":" move=> a x y.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18182"}},{"Add":{"text":" rewrite /nilpotent_weil_mul {2}/*:%R {4}/+%R; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18243"}},{"Add":{"text":" rewrite /ffun_scale /ffun_add.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18282"}},{"Add":{"text":" apply: eq_ffun => k.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18311"}},{"Add":{"text":" do 3 rewrite ffunE.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18339"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18340"}},{"Add":{"text":" rewrite scaler_sumr -big_split; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18387"}},{"Add":{"text":" apply: eq_bigr => i _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18418"}},{"Add":{"text":" rewrite scaler_sumr -big_split; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18465"}},{"Add":{"text":" apply: eq_bigr => j _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18496"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18497"}},{"Add":{"text":" case: (i + j + 1 == k)%N.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18531"}},{"Add":{"text":" + rewrite scalerAr -mulrDr.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18567"}},{"Add":{"text":" rewrite {1}/*:%R {1}/+%R; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18612"}},{"Add":{"text":" by rewrite /ffun_scale /ffun_add ffunE ffunE.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18670"}},{"Add":{"text":" + by rewrite addr0 scaler0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18706"}},{"Add":{"text":" Qed.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18715"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18716"}},{"Add":{"text":" Fact nilpotent_weil_mul_assoc n : associative (nilpotent_weil_mul n).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18790"}},{"Add":{"text":" Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18801"}},{"Add":{"text":" move=> x y z.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18823"}},{"Add":{"text":" apply: eq_ffun => k.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18852"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18853"}},{"Add":{"text":" suff: (\\sum_(i < n)\\sum_(j < n)\\sum_(i' < n)\\sum_(j' < n)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:18919"}},{"Add":{"text":" if (i + j + 1 == k)%N && (i' + j' + 1 == j)%N then x i * y i' * z j' else 0)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19008"}},{"Add":{"text":" = (\\sum_(i < n)\\sum_(j < n)\\sum_(i' < n)\\sum_(j' < n)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19074"}},{"Add":{"text":" if (i + j + 1 == k)%N && (i' + j' + 1 == i)%N then x i' * y j' * z j else 0).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19164"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19174"}},{"Add":{"text":" move=> eq.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19197"}},{"Add":{"text":" apply: Logic.eq_trans; first (apply: Logic.eq_trans; last apply: eq).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19279"}},{"Add":{"text":" - apply: eq_bigr => i _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19316"}},{"Add":{"text":" apply: eq_bigr => j _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19355"}},{"Add":{"text":" case: (i + j + 1 == k)%N.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19397"}},{"Add":{"text":" + rewrite ffunE mulr_sumr.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19440"}},{"Add":{"text":" apply: eq_bigr => i' _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19484"}},{"Add":{"text":" rewrite mulr_sumr.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19523"}},{"Add":{"text":" apply: eq_bigr => j' _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19567"}},{"Add":{"text":" case: (i' + j' + 1 == j)%N; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19622"}},{"Add":{"text":" * by rewrite mulrA.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19662"}},{"Add":{"text":" * by rewrite mulr0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19702"}},{"Add":{"text":" + rewrite big1; first done.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19746"}},{"Add":{"text":" move=> i' _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19779"}},{"Add":{"text":" by rewrite big1.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19816"}},{"Add":{"text":" - apply: eq_bigr => i _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19853"}},{"Add":{"text":" apply: eq_bigr => j _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19892"}},{"Add":{"text":" case: (i + j + 1 == k)%N.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19934"}},{"Add":{"text":" + rewrite ffunE mulr_suml.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:19977"}},{"Add":{"text":" apply: eq_bigr => i' _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20021"}},{"Add":{"text":" rewrite mulr_suml.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20060"}},{"Add":{"text":" apply: eq_bigr => j' _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20104"}},{"Add":{"text":" case: (i' + j' + 1 == i)%N; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20159"}},{"Add":{"text":" * done.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20187"}},{"Add":{"text":" * by rewrite mul0r.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20227"}},{"Add":{"text":" + rewrite big1; first done.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20271"}},{"Add":{"text":" move=> i' _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20304"}},{"Add":{"text":" by rewrite big1.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20341"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20351"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20352"}},{"Add":{"text":" have: forall (P : 'I_n -> bool) F, (forall a b, P a -> P b -> a = b)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20429"}},{"Add":{"text":" -> (\\sum_(i | P i) F i) = if [pick x | P x] is Some x then F x else 0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20512"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20522"}},{"Add":{"text":" move=> t P F eq.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20551"}},{"Add":{"text":" case pickP.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20575"}},{"Add":{"text":" - move=> i pf.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20602"}},{"Add":{"text":" apply: big_pred1.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20636"}},{"Add":{"text":" move=> j.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20662"}},{"Add":{"text":" apply/idP/eqP.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20693"}},{"Add":{"text":" + move=> pf2.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20723"}},{"Add":{"text":" by apply: eq.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20757"}},{"Add":{"text":" + by move=>->.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20788"}},{"Add":{"text":" - move=> H.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20812"}},{"Add":{"text":" by apply: big_pred0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20849"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20859"}},{"Add":{"text":" move=> lemma.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20881"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20882"}},{"Add":{"text":" suff: (\\sum_(i < n)\\sum_(i' < n)\\sum_(j' < n)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:20936"}},{"Add":{"text":" if (i + (i' + j' + 1) + 1 == k)%N then x i * y i' * z j' else 0)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21013"}},{"Add":{"text":" = (\\sum_(j < n)\\sum_(i' < n)\\sum_(j' < n)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21067"}},{"Add":{"text":" if ((i' + j' + 1) + j + 1 == k)%N then x i' * y j' * z j else 0).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21145"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21155"}},{"Add":{"text":" move=> eq.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21178"}},{"Add":{"text":" apply: Logic.eq_trans; first (apply: Logic.eq_trans; last apply: eq).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21260"}},{"Add":{"text":" - apply: eq_bigr => i _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21297"}},{"Add":{"text":" rewrite exchange_big; apply: eq_bigr => i' _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21359"}},{"Add":{"text":" rewrite exchange_big; apply: eq_bigr => j' _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21421"}},{"Add":{"text":" rewrite -big_mkcond.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21458"}},{"Add":{"text":" rewrite lemma.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21489"}},{"Add":{"text":" + case pickP.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21519"}},{"Add":{"text":" * move=> j /andP [/eqP <- /eqP <-].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21575"}},{"Add":{"text":" by case eqP.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21612"}},{"Add":{"text":" * case: eqP; last done.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21656"}},{"Add":{"text":" move=> eq2.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21692"}},{"Add":{"text":" suff: (i' + j' + 1)%N < n.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21743"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21769"}},{"Add":{"text":" move=> less nope.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21815"}},{"Add":{"text":" suff: false by [].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21862"}},{"Add":{"text":" rewrite -(nope (Ordinal less)) -eq2; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21934"}},{"Add":{"text":" by apply /andP.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:21978"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22004"}},{"Add":{"text":" apply: leq_ltn_trans; last exact: ltn_ord k.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22073"}},{"Add":{"text":" rewrite -eq2.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22111"}},{"Add":{"text":" apply: leq_trans; [apply: leq_addl | apply: leq_addr].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22190"}},{"Add":{"text":" + move=> [a a_pf] [b b_pf] /andP [/eqP <- /eqP ->] /andP [_ /eqP eq2].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22277"}},{"Add":{"text":" simpl in eq2.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22311"}},{"Add":{"text":" move: eq2 a_pf => -> a_pf.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22358"}},{"Add":{"text":" f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22387"}},{"Add":{"text":" apply: proof_irrelevance.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22433"}},{"Add":{"text":" - apply: Logic.eq_sym.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22468"}},{"Add":{"text":" rewrite exchange_big; apply: eq_bigr => j _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22529"}},{"Add":{"text":" rewrite exchange_big; apply: eq_bigr => i' _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22591"}},{"Add":{"text":" rewrite exchange_big; apply: eq_bigr => j' _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22653"}},{"Add":{"text":" rewrite -big_mkcond.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22690"}},{"Add":{"text":" rewrite lemma.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22721"}},{"Add":{"text":" + case pickP.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22751"}},{"Add":{"text":" * move=> i /andP [/eqP <- /eqP <-].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22807"}},{"Add":{"text":" by case eqP.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22844"}},{"Add":{"text":" * case: eqP; last done.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22888"}},{"Add":{"text":" move=> eq2.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22924"}},{"Add":{"text":" suff: (i' + j' + 1)%N < n.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:22975"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23001"}},{"Add":{"text":" move=> less nope.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23047"}},{"Add":{"text":" suff: false by [].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23094"}},{"Add":{"text":" rewrite -(nope (Ordinal less)) -eq2; simpl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23166"}},{"Add":{"text":" by apply /andP.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23210"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23236"}},{"Add":{"text":" apply: leq_ltn_trans; last exact: ltn_ord k.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23305"}},{"Add":{"text":" rewrite -eq2.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23343"}},{"Add":{"text":" apply: leq_trans; [apply: leq_addr | apply: leq_addr].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23422"}},{"Add":{"text":" + move=> [a a_pf] [b b_pf] /andP [/eqP <- /eqP ->] /andP [_ /eqP eq2].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23509"}},{"Add":{"text":" simpl in eq2.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23543"}},{"Add":{"text":" move: eq2 a_pf => -> a_pf.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23590"}},{"Add":{"text":" f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23619"}},{"Add":{"text":" apply: proof_irrelevance.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23665"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23675"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23676"}},{"Add":{"text":" apply: Logic.eq_sym.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23705"}},{"Add":{"text":" rewrite exchange_big; apply: eq_bigr => i _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23758"}},{"Add":{"text":" rewrite exchange_big; apply: eq_bigr => i' _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23812"}},{"Add":{"text":" apply: eq_bigr => j' _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23844"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23845"}},{"Add":{"text":" suff: (i + i' + 1 + j')%N = (i + (i' + j' + 1))%N by move=>->.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23916"}},{"Add":{"text":" do 3 rewrite -addnA; f_equal; f_equal.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23963"}},{"Add":{"text":" apply: addnC.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23985"}},{"Add":{"text":" Qed.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23994"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:23995"}},{"Add":{"text":" Fact nilpotent_weil_mul_comm n : commutative (nilpotent_weil_mul n).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24068"}},{"Add":{"text":" Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24079"}},{"Add":{"text":" move=> x y.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24099"}},{"Add":{"text":" apply: eq_ffun => k.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24128"}},{"Add":{"text":" rewrite exchange_big.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24158"}},{"Add":{"text":" apply: eq_bigr => i _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24189"}},{"Add":{"text":" apply: eq_bigr => j _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24220"}},{"Add":{"text":" move: (addnC j i) => ->.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24253"}},{"Add":{"text":" move: (mulrC (x j) (y i)) => ->.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24294"}},{"Add":{"text":" done.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24308"}},{"Add":{"text":" Qed.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24317"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24318"}},{"Add":{"text":" Fact nilpotent_weil_mul_nilpotent n x (xs : 'I_n -> _) ","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24378"}},{"Add":{"text":" : \\big[nilpotent_weil_mul n/x]_i xs i = 0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24429"}},{"Add":{"text":" Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24440"}},{"Add":{"text":" move: xs.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24458"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24459"}},{"Add":{"text":" suff: forall m xs (mn : m <= n) (i : 'I_n), i < m -> ","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24521"}},{"Add":{"text":" (\\big[nilpotent_weil_mul n/x]_(j : 'I_m) xs j) i = 0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24587"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24597"}},{"Add":{"text":" move=> H xs.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24622"}},{"Add":{"text":" rewrite -ffunP => i.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24655"}},{"Add":{"text":" rewrite (H n xs (leqnn n) i (ltn_ord i)).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24709"}},{"Add":{"text":" by rewrite /0; simpl; rewrite /ffun_zero ffunE.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24769"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24779"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24780"}},{"Add":{"text":" elim=> [|m IH] xs mn k pf.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24815"}},{"Add":{"text":" - done.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24831"}},{"Add":{"text":" - rewrite big_ord_recl ffunE.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24869"}},{"Add":{"text":" rewrite big1; first done.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24907"}},{"Add":{"text":" move=> i _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24931"}},{"Add":{"text":" rewrite big1; first done.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24969"}},{"Add":{"text":" move=> j _.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:24993"}},{"Add":{"text":" case eqP; last done.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25026"}},{"Add":{"text":" move=> eq.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25049"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25050"}},{"Add":{"text":" suff: (\\big[nilpotent_weil_mul n/x]_(i0 < m) ","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25108"}},{"Add":{"text":" xs (lift ord0 i0)) j = 0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25150"}},{"Add":{"text":" {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25164"}},{"Add":{"text":" move=>->.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25190"}},{"Add":{"text":" apply: mulr0.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25220"}},{"Add":{"text":" }","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25234"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25235"}},{"Add":{"text":" apply: IH.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25258"}},{"Add":{"text":" - by apply: ltnW.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25288"}},{"Add":{"text":" - rewrite -ltnS.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25317"}},{"Add":{"text":" apply: leq_ltn_trans; last apply: pf.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25371"}},{"Add":{"text":" move: eq => <-.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25403"}},{"Add":{"text":" rewrite addn1.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25434"}},{"Add":{"text":" apply leq_addl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25466"}},{"Add":{"text":" Qed.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25475"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25476"}},{"Add":{"text":" Definition nilpotent_weil (n : nat) : WeilData R := {|","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25535"}},{"Add":{"text":" Domain := [finType of 'I_n];","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25572"}},{"Add":{"text":" Mul := nilpotent_weil_mul n;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25609"}},{"Add":{"text":" Lin := nilpotent_weil_mul_linear n;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25653"}},{"Add":{"text":" Assoc := nilpotent_weil_mul_assoc n;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25698"}},{"Add":{"text":" Comm := nilpotent_weil_mul_comm n;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25741"}},{"Add":{"text":" Nilpotent := ex_intro _ _ (nilpotent_weil_mul_nilpotent n);","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25809"}},{"Add":{"text":" |}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25817"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25818"}},{"Add":{"text":" Definition nilpotent_weil_iso {n} : 'D_n <--> Spec R (Weil (nilpotent_weil n)).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25902"}},{"Add":{"text":" apply: iso_trans; last apply: reifyIso.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25950"}},{"Add":{"text":" refine({|","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:25968"}},{"Add":{"text":" Forward '(exist x pf) := exist _ [ffun i => x] _;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26030"}},{"Add":{"text":" Backward '(exist f morph) := exist _ (\\sum_i f i) _;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26095"}},{"Add":{"text":" |}).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26108"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26122"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26123"}},{"Add":{"text":" Definition KL_D {n} : (nilpotent n -> R) <--> ('I_n -> R).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26186"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26200"}},{"Add":{"text":" Theorem KL_D_back {n coeffs} {d : nilpotent n}","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26251"}},{"Add":{"text":" : Backward _ _ KL_D coeffs d = polynomial coeffs d.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26311"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26325"}},{"Add":{"text":" Definition atomicD {n} : Atomic 'D_n := {|","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26372"}},{"Add":{"text":" Amazing X := { amazing Spec R (Weil (nilpotent_weil n)), X };","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26442"}},{"Add":{"text":" amaze _ _ := iso_trans (iso_exp (iso_exp nilpotent_weil_iso)) amaze;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26519"}},{"Add":{"text":" |}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26527"}},{"Add":{"text":" ","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26532"}},{"Add":{"text":"End nilpotent_properties.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26558"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26559"}},{"Add":{"text":"Global Instance atomicD {n} : Atomic 'D_n := atomicD.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26613"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26614"}},{"Add":{"text":"Module Export Δ_properties : Δ_properties_sig.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26663"}},{"Add":{"text":" Definition Δ_weil (n : nat) : WeilData R.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26710"}},{"Add":{"text":" Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26721"}},{"Add":{"text":" refine ({|","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26740"}},{"Add":{"text":" Domain := [finType of 'I_n];","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26781"}},{"Add":{"text":" Mul := fun _ _ => 0;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26814"}},{"Add":{"text":" Lin := fun _ _ _ _ => Logic.eq_sym (Logic.eq_trans (addr0 _) (scaler0 _ _));","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26903"}},{"Add":{"text":" Assoc := fun _ _ _ => Logic.eq_refl;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26952"}},{"Add":{"text":" Comm := fun _ _ => Logic.eq_refl;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:26998"}},{"Add":{"text":" Nilpotent := ex_intro _ [finType of 'I_1] _","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27054"}},{"Add":{"text":" |}).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27067"}},{"Add":{"text":" move=> x xs.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27088"}},{"Add":{"text":" apply: big_ord_recl.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27117"}},{"Add":{"text":" Defined.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27130"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27131"}},{"Add":{"text":" Definition KL_Δ {n} : (Δ n -> R) <--> (R * ('I_n -> R)).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27194"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27208"}},{"Add":{"text":" Theorem KL_Δ_back {n coeffs} {d : Δ n}","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27253"}},{"Add":{"text":" : Backward _ _ KL_Δ coeffs d = fst coeffs + \\sum_i snd coeffs i * d i.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27333"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27347"}},{"Add":{"text":" Definition atomicΔ {n} : Atomic (Δ n).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27392"}},{"Add":{"text":" Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27406"}},{"Add":{"text":"End Δ_properties.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27425"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27426"}},{"Add":{"text":"Global Instance atomicΔ {n} : Atomic (Δ n) := atomicΔ.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27484"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27485"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27486"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27487"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27488"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27489"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27490"}},{"Add":{"text":"(* Can this be done?","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27511"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27512"}},{"Add":{"text":"#[refine]","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27522"}},{"Add":{"text":"Global Instance atomicD_union : Atomic 'D_∞ := {|","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27574"}},{"Add":{"text":" Amazing X := _;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27594"}},{"Add":{"text":" amaze _ _ := _;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27614"}},{"Add":{"text":"|}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27618"}},{"Add":{"text":"Admitted.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27628"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27629"}},{"Add":{"text":"*)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27632"}}]}},{"FileAdd":{"meta":{"basename":"axioms.v","metadata":0},"context":[{"change":0,"pos":20}],"contents":[{"Add":{"text":"From mathcomp Require Import ssralg ssreflect ssrfun.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27721"}},{"Add":{"text":"Require Import weil_algebras atomic.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27758"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27759"}},{"Add":{"text":"From Coq Require Export FunctionalExtensionality ProofIrrelevance Description.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27838"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27839"}},{"Add":{"text":"Open Scope R.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27853"}},{"Add":{"text":"Export GRing.Theory.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27874"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27875"}},{"Add":{"text":"(* The ring of numbers. *)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27902"}},{"Add":{"text":"Parameter R : comUnitRingType.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27933"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27934"}},{"Add":{"text":"Section WeilAxioms.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27954"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27955"}},{"Add":{"text":"Variable (W : WeilData R).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27982"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:27983"}},{"Add":{"text":"Definition Spec (R : ringType) (A : algType R) := {lrmorphism A -> R^o}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28056"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28057"}},{"Add":{"text":"(* Axiom 1W, from *Synthetic Differential Geometry*. *)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28113"}},{"Add":{"text":"Definition KL_inv : Weil W -> (Spec R (Weil W) -> R) := fun a f => f a.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28185"}},{"Add":{"text":"Axiom KL : (Spec R (Weil W) -> R) -> Weil W.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28230"}},{"Add":{"text":"Axiom KL_linv : cancel KL_inv KL.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28264"}},{"Add":{"text":"Axiom KL_rinv : cancel KL KL_inv.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28298"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28299"}},{"Add":{"text":"(* Axiom 3, from *Synthetic Differential Geometry*. *)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28354"}},{"Add":{"text":"Axiom atomicAxiom : Atomic (Spec R (Weil W)).","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28400"}},{"Add":{"text":"End WeilAxioms.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28416"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28417"}},{"Add":{"text":"Global Instance iSpec {W} : Atomic (Spec R (Weil W)) := atomicAxiom W.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28488"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28489"}}]}},{"FileAdd":{"meta":{"basename":"atomic.v","metadata":0},"context":[{"change":0,"pos":20}],"contents":[{"Add":{"text":"From Coq Require Import PropExtensionality FunctionalExtensionality ProofIrrelevance ssreflect.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28620"}},{"Add":{"text":"Require Export isomorphism.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28648"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28649"}},{"Add":{"text":"Class Atomic (O : Type) := {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28678"}},{"Add":{"text":" Amazing : Type -> Type;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28706"}},{"Add":{"text":" amaze : forall {A B}, ((O -> A) -> B) <--> (A -> Amazing B);","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28771"}},{"Add":{"text":"}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28774"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28775"}},{"Add":{"text":"Notation \"{ 'amazing' O , X }\" := (Amazing (O := O) X)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28830"}},{"Add":{"text":" (at level 0, format \"{ 'amazing' O , X }\") : type_scope.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28891"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28892"}},{"Add":{"text":" ","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28897"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28898"}},{"Add":{"text":"#[refine]","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28908"}},{"Add":{"text":"Global Instance iUnit : Atomic unit := {","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28949"}},{"Add":{"text":" Amazing T := T;","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28969"}},{"Add":{"text":" amaze _ _ := {|","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:28989"}},{"Add":{"text":" Forward f t := f (fun 'tt => t);","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29030"}},{"Add":{"text":" Backward f t := f (t tt);","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29064"}},{"Add":{"text":" |}","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29071"}},{"Add":{"text":"}.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29074"}},{"Add":{"text":"Proof.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29081"}},{"Add":{"text":" - move=> f.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29097"}},{"Add":{"text":" apply: functional_extensionality => x.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29144"}},{"Add":{"text":" suff: x = fun 'tt => x tt by move=>->.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29191"}},{"Add":{"text":" apply: functional_extensionality.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29233"}},{"Add":{"text":" by move=>[].","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29254"}},{"Add":{"text":" - done.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29266"}},{"Add":{"text":"Qed.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29271"}}]}},{"FileAdd":{"meta":{"basename":"_CoqProject","metadata":0},"context":[{"change":2,"pos":1}],"contents":[{"Add":{"text":"theories/isomorphism.v","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29331"}},{"Add":{"text":"theories/atomic.v","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29349"}},{"Add":{"text":"theories/weil_algebras.v","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29374"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29375"}},{"Add":{"text":"theories/axioms.v","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29393"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29394"}},{"Add":{"text":"theories/basic_infinitesimal_spaces.v","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29432"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29433"}},{"Add":{"text":"theories/common.v","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29451"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29452"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29453"}},{"Add":{"text":"-R theories iris_internal_logic","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29485"}}]}},{"FileAdd":{"meta":{"basename":"README.md","metadata":0},"context":[{"change":2,"pos":1}],"contents":[{"Add":{"text":"Experimenting with synthetic differential geometry.","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29572"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29573"}},{"Add":{"text":"Useful book on the subject:","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29601"}},{"Add":{"text":"- Anders Kock, [Synthetic Differential Geometry](home.imf.au.dk/kock/sdg99.pdf), Cambridge University Press 1981, 2006","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29720"}}]}},{"FileAdd":{"meta":{"basename":"Makefile","metadata":0},"context":[{"change":2,"pos":1}],"contents":[{"Add":{"text":"# KNOWNTARGETS will not be passed along to CoqMakefile","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29810"}},{"Add":{"text":"KNOWNTARGETS := CoqMakefile","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29838"}},{"Add":{"text":"# KNOWNFILES will not get implicit targets from the final rule, and so","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29909"}},{"Add":{"text":"# depending on them won't invoke the submake","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:29954"}},{"Add":{"text":"# Warning: These files get declared as PHONY, so any targets depending","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30025"}},{"Add":{"text":"# on them always get rebuilt","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30054"}},{"Add":{"text":"KNOWNFILES := Makefile _CoqProject","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30091"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30092"}},{"Add":{"text":".DEFAULT_GOAL := invoke-coqmakefile","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30128"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30129"}},{"Add":{"text":"CoqMakefile: Makefile _CoqProject","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30163"}},{"Add":{"text":"\t$(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30216"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30217"}},{"Add":{"text":"invoke-coqmakefile: CoqMakefile","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30249"}},{"Add":{"text":"\t$(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30340"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30341"}},{"Add":{"text":".PHONY: invoke-coqmakefile $(KNOWNFILES)","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30382"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30383"}},{"Add":{"text":"####################################################################","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30452"}},{"Add":{"text":"## Your targets here ##","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30521"}},{"Add":{"text":"####################################################################","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30590"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30591"}},{"Add":{"text":"# This should be the last rule, to handle any targets not declared above","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30664"}},{"Add":{"text":"%: invoke-coqmakefile","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30686"}},{"Add":{"text":"\t@true","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30693"}}]}},{"FileAdd":{"meta":{"basename":".ignore","metadata":0},"context":[{"change":2,"pos":1}],"contents":[{"Add":{"text":".git","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30731"}},{"Add":{"text":".DS_Store","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30741"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30742"}},{"Add":{"text":"CoqMakefile","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30754"}},{"Add":{"text":"CoqMakefile.conf","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30771"}},{"Add":{"text":"","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30772"}},{"Add":{"text":"*.vo","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30777"}},{"Add":{"text":"*.vos","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30783"}},{"Add":{"text":"*.vok","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30789"}},{"Add":{"text":"*.glob","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30796"}},{"Add":{"text":"*.aux","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30802"}},{"Add":{"text":"*.d","pos":"52ASAKJIIII33LAKTLTU7WM53UA7F45RJKV6I3J46QGVMGQDMOCQC:30806"}}]}}],"owner":"finegeometer","repo":"synthetic-differential-geometry","token":"KI+YZ9qzVAUxe+K5uRIiiDyzvui3GRhmnHSTCK7UnmI=","login":null}

…

Dependencies

Change contents

Review