Commit 2021-11-10 14:52 8aadbcb7

View on Github →

feat(linear_algebra/*_algebra): add some simp lemmas about the algebra map and generators of free constructions (#10247) These are quite repetitive, but I'm not sure how to generalize

Estimated changes

Modified src/algebra/free_algebra.lean

added theorem free_algebra.algebra_map_eq_one_iff

added theorem free_algebra.algebra_map_eq_zero_iff

added theorem free_algebra.algebra_map_inj

added theorem free_algebra.ι_inj

added theorem free_algebra.ι_ne_algebra_map

added theorem free_algebra.ι_ne_one

added theorem free_algebra.ι_ne_zero

Modified src/linear_algebra/exterior_algebra.lean

added theorem exterior_algebra.algebra_map_eq_one_iff

added theorem exterior_algebra.algebra_map_eq_zero_iff

added theorem exterior_algebra.algebra_map_inj

added def exterior_algebra.to_triv_sq_zero_ext

added theorem exterior_algebra.to_triv_sq_zero_ext_ι

added theorem exterior_algebra.ι_eq_algebra_map_iff

added theorem exterior_algebra.ι_eq_zero_iff

added theorem exterior_algebra.ι_inj

added theorem exterior_algebra.ι_ne_one

added theorem exterior_algebra.ι_range_disjoint_one

Modified src/linear_algebra/tensor_algebra.lean

added theorem tensor_algebra.algebra_map_eq_one_iff

added theorem tensor_algebra.algebra_map_eq_zero_iff

added theorem tensor_algebra.algebra_map_inj

added def tensor_algebra.to_triv_sq_zero_ext

added theorem tensor_algebra.to_triv_sq_zero_ext_ι

added theorem tensor_algebra.ι_eq_algebra_map_iff

added theorem tensor_algebra.ι_eq_zero_iff

added theorem tensor_algebra.ι_inj

added theorem tensor_algebra.ι_ne_one

added theorem tensor_algebra.ι_range_disjoint_one