QuadraticAlgebra 📖 | CompData | 118 mathmath: QuadraticAlgebra.coe_sub, QuadraticAlgebra.instIsScalarTower, QuadraticAlgebra.coe_mul_eq_smul, QuadraticAlgebra.im_intCast, QuadraticAlgebra.C_eq_zero_iff, QuadraticAlgebra.instNontrivial, QuadraticAlgebra.C_pow, QuadraticAlgebra.coe_one, QuadraticAlgebra.coe_mul, QuadraticAlgebra.algebraMap_inj, QuadraticAlgebra.norm_algebraMap, QuadraticAlgebra.mk_add_mk, QuadraticAlgebra.C_add, QuadraticAlgebra.zsmul_val, QuadraticAlgebra.linearEquivTuple_apply, QuadraticAlgebra.norm_zero, QuadraticAlgebra.instFinite, QuadraticAlgebra.nsmul_mk, QuadraticAlgebra.algebraMap_re, QuadraticAlgebra.omega_mul_coe_mul_mk, QuadraticAlgebra.algebraMap_dvd_iff, QuadraticAlgebra.mul_coe_eq_smul, QuadraticAlgebra.C_eq_algebraMap, QuadraticAlgebra.norm_eq_one_iff_mem_unitary, QuadraticAlgebra.imₗ_apply, QuadraticAlgebra.instFree, QuadraticAlgebra.re_zero, QuadraticAlgebra.C_mul, QuadraticAlgebra.equivProd_symm_apply, QuadraticAlgebra.lift_apply_apply, QuadraticAlgebra.neg_mk, QuadraticAlgebra.coe_eq_one_iff, QuadraticAlgebra.norm_neg, QuadraticAlgebra.C_sub, QuadraticAlgebra.C_eq_one_iff, QuadraticAlgebra.reₗ_apply, QuadraticAlgebra.star_mem_nonZeroDivisors_iff, QuadraticAlgebra.star_mk, QuadraticAlgebra.C_neg, QuadraticAlgebra.C_natCast, QuadraticAlgebra.rank_eq_two, QuadraticAlgebra.coe_neg, QuadraticAlgebra.coe_dvd_iff_dvd, QuadraticAlgebra.mul_star, QuadraticAlgebra.smul_C, QuadraticAlgebra.im_smul, QuadraticAlgebra.im_neg, QuadraticAlgebra.C_injective, QuadraticAlgebra.mk_sub_mk, QuadraticAlgebra.norm_natCast, QuadraticAlgebra.norm_coe, QuadraticAlgebra.isUnit_iff_norm_isUnit, QuadraticAlgebra.C_intCast, QuadraticAlgebra.basis_repr_apply, QuadraticAlgebra.C_mul_eq_smul, QuadraticAlgebra.coe_norm_eq_mul_star, QuadraticAlgebra.algebraMap_eq, QuadraticAlgebra.re_neg, QuadraticAlgebra.re_star, QuadraticAlgebra.lift_symm_apply_coe, QuadraticAlgebra.im_one, QuadraticAlgebra.coe_natCast, QuadraticAlgebra.smul_coe, QuadraticAlgebra.omega_mul_omega_eq_mk, QuadraticAlgebra.coe_add, QuadraticAlgebra.norm_intCast, QuadraticAlgebra.mker_norm_eq_unitary, QuadraticAlgebra.linearEquivTuple_symm_apply, QuadraticAlgebra.re_smul, QuadraticAlgebra.im_mul, QuadraticAlgebra.mk_mul_mk, QuadraticAlgebra.omega_mul_algebraMap_mul_mk, QuadraticAlgebra.instCharZero, QuadraticAlgebra.im_zero, QuadraticAlgebra.C_one, QuadraticAlgebra.coe_pow, QuadraticAlgebra.algHom_ext_iff, QuadraticAlgebra.instSMulCommClass, QuadraticAlgebra.mul_C_eq_smul, QuadraticAlgebra.coe_intCast, QuadraticAlgebra.norm_def, QuadraticAlgebra.re_sub, QuadraticAlgebra.norm_one, QuadraticAlgebra.algebraMap_dvd_iff_dvd, QuadraticAlgebra.mk_eq_add_smul_omega, QuadraticAlgebra.re_natCast, QuadraticAlgebra.instIsTorsionFree, QuadraticAlgebra.finrank_eq_two, QuadraticAlgebra.im_sub, QuadraticAlgebra.coe_mem_nonZeroDivisors_iff, QuadraticAlgebra.norm_star, QuadraticAlgebra.algebraMap_norm_eq_mul_star, QuadraticAlgebra.instSubsingleton, QuadraticAlgebra.re_add, QuadraticAlgebra.C_smul, QuadraticAlgebra.re_one, QuadraticAlgebra.algebraMap_mem_nonZeroDivisors_iff, QuadraticAlgebra.coe_algebraMap, QuadraticAlgebra.det_toLinearMap_eq_norm, QuadraticAlgebra.re_mul, QuadraticAlgebra.smul_mk, QuadraticAlgebra.coe_injective, QuadraticAlgebra.omega_mul_mk, QuadraticAlgebra.im_natCast, QuadraticAlgebra.norm_mem_nonZeroDivisors_iff, QuadraticAlgebra.omega_mul_omega_eq_add, QuadraticAlgebra.im_add, QuadraticAlgebra.coe_eq_zero_iff, QuadraticAlgebra.C_zero, QuadraticAlgebra.norm_eq_zero_iff_eq_zero, QuadraticAlgebra.im_star, QuadraticAlgebra.instIsCentralScalar, QuadraticAlgebra.coe_zero, QuadraticAlgebra.coe_dvd_iff, QuadraticAlgebra.coe_smul, QuadraticAlgebra.algebraMap_im, QuadraticAlgebra.re_intCast, QuadraticAlgebra.algebraMap_injective
|