Theorem Complex.det_conjAe

Modification history

2026-05-21 08:11
Mathlib/LinearAlgebra/Complex/Determinant.lean
refactor(Algebra): replace `SemilinearEquivClass.semilinearEquiv` by structure-specific coercions (#37944) …
Modified Complex.det_conjAeView on Github →
2023-05-03 01:24
Mathlib/Data/Complex/Determinant.lean
feat: port Data.Complex.Determinant (#3765)
Added Complex.det_conjAeView on Github →