Def Counterexample.withSign.independent

Modification history

2026-08-04 17:34
Counterexamples/DirectSumIsInternal.lean
chore(Counterexamples/DirectSumIsInternal): automated extraction from #42430 (#42431) …
Deleted Counterexample.withSign.independentView on Github →
2026-06-18 23:59
Counterexamples/DirectSumIsInternal.lean
chore: bump toolchain to v4.32.0-rc1 (#40732)
Added Counterexample.withSign.independentView on Github →
2026-06-15 00:50
Counterexamples/DirectSumIsInternal.lean
chore(Counterexamples/DirectSumIsInternal): fix defLemma error (#40592) …
Deleted Counterexample.withSign.independentView on Github →
2024-11-25 10:13
Counterexamples/DirectSumIsInternal.lean
chore: rename `CompleteLattice.Independent`/`.SetIndependent` to `iSupIndep`/`sSupIndep` (#19409) …
Modified Counterexample.withSign.independentView on Github →
2023-06-16 10:33
Counterexamples/DirectSumIsInternal.lean
feat: port Counterexamples.DirectSumIsInternal (#4812)
Added Counterexample.withSign.independentView on Github →