Commit 2023-06-05 05:13 041a489d

View on Github →

feat: port Algebra.Symmetrized (#4632)

Estimated changes

added theorem SymAlg.invOf_sym
added theorem SymAlg.mul_comm
added theorem SymAlg.mul_def
added def SymAlg.sym
added theorem SymAlg.sym_add
added theorem SymAlg.sym_bijective
added theorem SymAlg.sym_comp_unsym
added theorem SymAlg.sym_eq_one_iff
added theorem SymAlg.sym_inj
added theorem SymAlg.sym_injective
added theorem SymAlg.sym_inv
added theorem SymAlg.sym_mul_self
added theorem SymAlg.sym_mul_sym
added theorem SymAlg.sym_ne_one_iff
added theorem SymAlg.sym_neg
added theorem SymAlg.sym_one
added theorem SymAlg.sym_smul
added theorem SymAlg.sym_sub
added theorem SymAlg.sym_surjective
added theorem SymAlg.sym_symm
added theorem SymAlg.sym_unsym
added def SymAlg.unsym
added theorem SymAlg.unsym_add
added theorem SymAlg.unsym_bijective
added theorem SymAlg.unsym_comp_sym
added theorem SymAlg.unsym_inj
added theorem SymAlg.unsym_injective
added theorem SymAlg.unsym_inv
added theorem SymAlg.unsym_mul
added theorem SymAlg.unsym_mul_self
added theorem SymAlg.unsym_neg
added theorem SymAlg.unsym_one
added theorem SymAlg.unsym_smul
added theorem SymAlg.unsym_sub
added theorem SymAlg.unsym_sym
added theorem SymAlg.unsym_symm
added def SymAlg