Commit 2023-06-16 10:33 7fb05c08

View on Github →

feat: port Counterexamples.DirectSumIsInternal (#4812)

Estimated changes

Modified Counterexamples.lean

Created Counterexamples/DirectSumIsInternal.lean

added theorem Counterexample.UnitsInt.one_ne_neg_one

added theorem Counterexample.mem_withSign_neg_one

added theorem Counterexample.mem_withSign_one

added theorem Counterexample.withSign.iSup

added def Counterexample.withSign.independent

added theorem Counterexample.withSign.isCompl

added theorem Counterexample.withSign.not_injective

added theorem Counterexample.withSign.not_internal

added def Counterexample.withSign