Adam Topaz

`lake new foo math` can cause a mismatch in Lean4 versions.

3

`lake new foo math` creates a folder `foo` with a `lean-toolchain` file based on the version of Lean used to invoke `lake`, while also adding `mathlib4` as a dependency. The...

feat(ring_theory/valuation/valuation_subring): Supremum of families of valuation rings.

1

Adds two definitions: - The supremum of a directed family of valuation rings, as a valuation ring. - The supremum of a family of valuation rings which are bounded below...

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