damiano
damiano
The possibilities are `set.univ, U, Uᶜ, ∅`, This lemma is from LTE. --- [](https://gitpod.io/from-referrer/)
This lemma is extracted from #15984, as suggested by the code-review. --- [](https://gitpod.io/from-referrer/)
This PR constructs a linear order on `finsupp`s where both source and target are linearly ordered. This is useful for #15983, where these linear orders are used to prove that...
From LTE Author: Johan Commelin [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/extremally.20disconnected.20sets) --- [](https://gitpod.io/from-referrer/)
This PR proves that the lexicographic linear order on finitely supported functions preserves (one) covariant class assumption. This is a further step in proving that many `add_monoid_algebra`s have no zero-divisors....
This PR defines 1. the `sup_degree` of an `add_monoid_algebra`, graded by a `semilattice_sup`; 1. the `inf_degree` of an `add_monoid_algebra`, graded by a `semilattice_inf`; 1. the `max_degree` of an `add_monoid_algebra`, graded...
The six lemmas in this PR show that * `finset.max` and `finset.max'` coincide (when and how they can); * the `finset.max'` of `s.erase x` is not `x`; * the `finset.max`...
--- [](https://gitpod.io/from-referrer/)
Dear Kevin, below is the diff between the file src/complex/Level_00_basic.lean in your repository and the one where I corrected a couple of typos. If you prefer, I can also send...
The 'lemma' command elaborates as 'theorem' but gives warning + codeaction to use 'theorem' instead. I am picking up @jcommelin's PR #413, but I did not know how to modify...