Eric Wieser

refactor(module/submodule): allow submodules to be used for sub-distrib_mul_actions

2

--- - [x] depends on: #6648 note that this only deals with `submonoid`s closed under smul, not `subgroup`s closed under smul; I know one of @kbuzzard's students is working on...

This generalizes `multilinear_map.dom_coprod` to maps with non-uniform argument types, at the expense of introducing unpleasant `sum.elim M N` pi-types --- [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/The.20tensor.20product.20of.20two.20multilinear.20maps.20is.20a.20multiline.2E.2E.2E/near/218474366)

feat(topology,analysis): add the discrete metric and normed spaces

6

These are provided as definitions for now, but in future might be reasonable to associate with a type synonym. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Discrete.20metric.2E/near/281044832) --- - [x] depends on: #13927 - [x] depends on:...

This aims to generalize some of the `nnreal_binary` stuff in LTE. https://github.com/leanprover-community/lean-liquid/blob/b9b42a840d2416657d7ba173f5d20e24906e6137/src/for_mathlib/nnreal_int_binary.lean#L136-L140 --- [](https://gitpod.io/from-referrer/)

refactor(linear_algebra/clifford_algebra): relax typeclasses to semiring

1

This generalization isn't motivated by any particular result or generalization in the literature; rather, it's motivated by allowing `exterior_algebra R M` to be redefined as `clifford_algebra 0`, as this prevents...

fix: respect type reducibility when generating injectivity lemmas

2

The relevant test case is: ```lean def WrappedNat (_n : Nat) := Nat structure WithWrapped : Type := (n : Nat) (m : WrappedNat n) #check WithWrapped.mk.injEq #print WithWrapped.noConfusionType ```...

doc: upstream the Lean4 pygments lexer

5

An improved `lean4` lexer is now part of pygments. This depends on https://github.com/pygments/pygments/pull/2618 (now merged), and [a subsequent release](https://github.com/pygments/pygments/milestone/23)

fix: collect level parameters in evalExpr

9

`elabEvalUnsafe` already does something similar: it also instantiates universe metavariables, but it is not clear to me whether that is sensible here. To be conservative, I leave it out of...

feat: allow `EStateM` to be used polymorphically

1

This doesn't change `IO` or `ST`, but does enable downstream projects like `Mathlib` to use `EStateM` for their own purposes with full universe polymorphism. The alternative is defining an entire...

feat: Implement `extends flat`

1

This implements https://github.com/leanprover/lean4/issues/2666, allowing manual tweaking of whether structure inheritance is flat or nested, without forcing the user to fallback to the `FlatHack` approach in https://arxiv.org/abs/2306.00617. This is documented via...