OAI/Combinatorics/HadwigerCounterexample/MatrixRanks.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.rk_surj line 17
2. theorem OAI.HadwigerCounterexample.rk_inj line 23
3. theorem OAI.HadwigerCounterexample.rk_comp_le_right line 32
4. theorem OAI.HadwigerCounterexample.rk_comp_le_left line 37
5. theorem OAI.HadwigerCounterexample.rk_add_le line 41
6. theorem OAI.HadwigerCounterexample.rank_cast line 55
7. theorem OAI.HadwigerCounterexample.dim_vec line 56
8. theorem OAI.HadwigerCounterexample.mrk_inj line 60
9. theorem OAI.HadwigerCounterexample.mrk_surj line 62
10. theorem OAI.HadwigerCounterexample.transpose_surj_iff line 65
11. theorem OAI.HadwigerCounterexample.mrk_add_le line 68
12. abbrev OAI.HadwigerCounterexample.colSp line 71
13. theorem OAI.HadwigerCounterexample.colSp_dim line 73
14. theorem OAI.HadwigerCounterexample.colSp_mem line 76
15. def OAI.HadwigerCounterexample.pack line 81

    Source documentation

    A coordinate set of basis vectors of a subspace arranged as columns.

    def pack (S : Space (Vec I)) : Mat I (Fin (dim S)) :=
    …

    Mentions: OAI.HadwigerCounterexample.Space, OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.dim

16. theorem OAI.HadwigerCounterexample.pack_eq line 86
17. theorem OAI.HadwigerCounterexample.pack_inj line 93
18. theorem OAI.HadwigerCounterexample.colSp_pack line 99
19. theorem OAI.HadwigerCounterexample.inj_comp_mat line 106

    Source documentation

    Matrix multiplication cancels when a left factor is injective.

    theorem inj_comp_mat [Fintype K] (A : Mat I J) (B : Mat J K)
        (hA : Injective A.mulVec) (hB : Injective B.mulVec) :
        Injective (A*B).mulVec := by
    …

    Mentions: OAI.HadwigerCounterexample.Mat

20. theorem OAI.HadwigerCounterexample.coe_mv_inj line 113
21. theorem OAI.HadwigerCounterexample.toMat_map line 119
22. theorem OAI.HadwigerCounterexample.frame_move line 124

    Source documentation

    Paired-frame transitivity of §3 in matrix form.

    theorem frame_move [Fintype K] [DecidableEq K] {A A' : Mat K I} {B B' : Mat K J}
        (ha : Injective A.mulVec) (ha' : Injective A'.mulVec) (hb : Injective B.mulVec)
        (hb' : Injective B'.mulVec) (h : Aᵀ * B = A'ᵀ * B') :
        ∃ L R : Mat K K, L*R = 1 ∧ R*L = 1 ∧ L*A=A' ∧ Rᵀ*B = B' := by
    …

    Mentions: OAI.HadwigerCounterexample.Mat