Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-30 11:26 db059004

View on Github →

feat(linear_algebra/clifford_algebra): two algebras are isomorphic if their quadratic forms are equivalent (#8128)

Estimated changes

Modified src/linear_algebra/clifford_algebra/basic.lean

added def clifford_algebra.equiv_of_isometry

added theorem clifford_algebra.equiv_of_isometry_refl

added theorem clifford_algebra.equiv_of_isometry_symm

added theorem clifford_algebra.equiv_of_isometry_trans

added def clifford_algebra.map

added theorem clifford_algebra.map_apply_ι

added theorem clifford_algebra.map_comp_map

added theorem clifford_algebra.map_comp_ι

added theorem clifford_algebra.map_id