proofs(lean4): land the green half of the η extension (PARTIAL — ET-1..3 η)#34

hyperpolymath merged 1 commit into

mainhyperpolymath/systemet:mainfrom

proofs/l1-eta-extensionhyperpolymath/systemet:proofs/l1-eta-extensionCopy head branch name to clipboard