Commit 2022-09-29 12:54 2e09d790

View on Github →

feat(topology/algebra/algebra): algebra_clm does not need a normed space or field (#16690) This also clean up the variables in the topology/algebra/algebra.lean file, to ensure that the type variables come first (as this is a useful convention for when using @ notation).

Estimated changes