Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.det_conj_lie

Modification history

2023-01-24 03:14
src/analysis/complex/basic.lean
refactor(analysis/complex/basic, data/complex/is_R_or_C): downgrade imports (#18217) …
Modified complex.det_conj_lieView on Github →
2022-01-12 07:31
src/analysis/complex/basic.lean
feat(analysis/complex/basic): determinant of `conj_lie` (#11389) …
Added complex.det_conj_lieView on Github →