OAI/Combinatorics/PolynomialVacuum/Algebra/Scalars.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumAlgebra.q_ne_zero line 7
  2. theorem OAI.PolynomialVacuumAlgebra.q_pow_four line 9
  3. theorem OAI.PolynomialVacuumAlgebra.q_pow_eight line 15
  4. theorem OAI.PolynomialVacuumAlgebra.q_pow_sixteen line 20
  5. theorem OAI.PolynomialVacuumAlgebra.q_inv line 25
  6. theorem OAI.PolynomialVacuumAlgebra.q_four_inv line 32
  7. theorem OAI.PolynomialVacuumAlgebra.q_five_inv line 35
  8. theorem OAI.PolynomialVacuumAlgebra.q_plus_inv line 42
  9. theorem OAI.PolynomialVacuumAlgebra.sqrt_two_pos line 53
  10. theorem OAI.PolynomialVacuumAlgebra.sqrt_two_sq line 54
  11. theorem OAI.PolynomialVacuumAlgebra.sqrt_two_ne_one line 55
  12. theorem OAI.PolynomialVacuumAlgebra.xStar_mul_q_sum line 59
  13. theorem OAI.PolynomialVacuumAlgebra.q_two_sum line 64
  14. theorem OAI.PolynomialVacuumAlgebra.xStar_sq_mul_sqrt_two line 79
  15. theorem OAI.PolynomialVacuumAlgebra.xStar_sq_twice line 89
  16. theorem OAI.PolynomialVacuumAlgebra.nZero_ne_zero line 99
  17. theorem OAI.PolynomialVacuumAlgebra.t_ne_zero line 103
  18. theorem OAI.PolynomialVacuumAlgebra.T_ne_zero line 104