Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-27 08:42 fcb37903

View on Github →

feat(topology/algebra/matrix): the determinant is a continuous map (#10503) Formalized as part of the Sphere Eversion project.

Estimated changes

Modified src/linear_algebra/matrix/determinant.lean

added theorem matrix.coe_det_is_empty

Created src/topology/algebra/matrix.lean

added theorem continuous_det

Modified src/topology/constructions.lean

added theorem continuous_apply_apply