Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-05 12:24 a0cb45fe

View on Github →

feat(linear_algebra/clifford_algebra): the reals and complex numbers have isomorphic real clifford algebras (#8165)

Estimated changes

Created src/linear_algebra/clifford_algebra/equivs.lean

added def clifford_algebra_complex.Q

added theorem clifford_algebra_complex.Q_apply

added def clifford_algebra_complex.to_complex

added theorem clifford_algebra_complex.to_complex_ι

added theorem clifford_algebra_ring.ι_eq_zero