Commit 2023-05-03 01:24 775b745f

View on Github →

feat: port Data.Complex.Determinant (#3765)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Complex/Determinant.lean

added theorem Complex.det_conjAe

added theorem Complex.linearEquiv_det_conjAe