mathlib

mathlib copied to clipboard

Change the behavior of the infoview to visually distinguish: * frozen instances * typeclass assumptions that are not instances * unfrozen typeclass assumptions * non typeclass assumptions --- The style...

YaelDillies

feat(analysis/normed/group/basic): Multiplicative, noncommutative normed groups

1

Define * `seminormed_group` * `seminormed_add_group` * `seminormed_comm_group` * `normed_group` * `normed_add_group` * `normed_comm_group` Additivize all lemmas in `analysis.normed.group.basic`. To disambiguate names, I add one or two `'` to the multiplicative...

YaelDillies

feat(data/finsupp/lex): linear order on finsupps

7

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...

adomani

feat(ring_theory/finiteness): A morphism is finitely presented if the composition with a finite morphism is.

5

--- [](https://gitpod.io/from-referrer/)

erdOne

refactor(data/int/cast): Use hom classes

6

Restate lemmas using `monoid_with_zero_hom_class`/`ring_hom_class` instead of `monoid_with_zero_hom`/`ring_hom`. --- - [ ] depends on: #15985 [](https://gitpod.io/from-referrer/)

YaelDillies

Define `pfun.prod : (α →. γ) → (β →. δ) → α × β →. γ × δ`. --- [](https://gitpod.io/from-referrer/)

YaelDillies

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/)

adomani

chore(*): Rename `is_scalar_tower` to `smul_assoc_class`

1

to match `smul_comm_class` and `vadd_assoc_class`. --- [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/left.20vs.20right.20modules.20in.20tensor.20products/near/261974400), [other Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/smul_assoc_class) [](https://gitpod.io/from-referrer/)

YaelDillies

chore(combinatorics/*): Fix lint

4

Fix the linting errors coming from `fintype_finite`, `to_additive_doc` and `doc_blame`. Pull out a `[projective_plane P L]` assumption to a `variables` declaration in `combinatorics.configuration`. --- [](https://gitpod.io/from-referrer/)

YaelDillies

feat(data/finsupp/witnesses): new file to prove results about linear orders and covariant classes in finsupps

1

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....

adomani