OAI/LinearAlgebra/CirculantHadamard/Witnesses.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CirculantHadamard.firstRow_one line 9
2. def OAI.CirculantHadamard.firstRow_four line 11
3. def OAI.CirculantHadamard.witness_one line 13
4. def OAI.CirculantHadamard.witness_four line 15
5. theorem OAI.CirculantHadamard.witness_one_first_row line 21
6. theorem OAI.CirculantHadamard.witness_four_first_row line 23
7. theorem OAI.CirculantHadamard.witness_one_eq_rowCirculant line 25
8. theorem OAI.CirculantHadamard.witness_four_eq_rowCirculant line 29
9. theorem OAI.CirculantHadamard.witness_one_signs line 33
10. theorem OAI.CirculantHadamard.witness_four_signs line 36
11. theorem OAI.CirculantHadamard.witness_one_gram line 39
12. theorem OAI.CirculantHadamard.witness_four_gram line 46
13. theorem OAI.CirculantHadamard.witness_one_isCirculant line 54
14. theorem OAI.CirculantHadamard.witness_four_isCirculant line 58
15. theorem OAI.CirculantHadamard.witness_one_isSignHadamard line 62
16. theorem OAI.CirculantHadamard.witness_four_isSignHadamard line 65
17. theorem OAI.CirculantHadamard.exists_one line 68
18. theorem OAI.CirculantHadamard.exists_four line 71
19. theorem OAI.CirculantHadamard.exists_of_order_one_or_four line 75

    Source documentation

    The explicit matrices of orders one and four establish existence.

    theorem exists_of_order_one_or_four {n : ℕ} (hn : n = 1 ∨ n = 4) :
        ExistsRealCirculantHadamard n := by
    …

    Mentions: OAI.CirculantHadamard.ExistsRealCirculantHadamard