OAI/Topology/CoarseAssembly/CongruenceElementary.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoarseAssembly.reduce_transvection line 14
2. lemma OAI.CoarseAssembly.transvection_mem_elementaryReduction line 22
3. lemma OAI.CoarseAssembly.elementaryReduction_zero_surjective line 30
4. lemma OAI.CoarseAssembly.elementaryReduction_one_surjective line 34
5. lemma OAI.CoarseAssembly.elementary_row_same line 60
6. lemma OAI.CoarseAssembly.elementary_row_other line 66
7. lemma OAI.CoarseAssembly.upperUnitriangular_mem_elementaryReduction line 72
8. lemma OAI.CoarseAssembly.diagonal_mem_elementaryReduction line 91
9. def OAI.CoarseAssembly.secondDiagonal line 128
10. lemma OAI.CoarseAssembly.secondDiagonal_mem_elementaryReduction line 132
11. lemma OAI.CoarseAssembly.upperTriangular_mem_elementaryReduction line 169
12. lemma OAI.CoarseAssembly.isUnit_of_mod_two_one line 205
13. lemma OAI.CoarseAssembly.mod_two_identity_entry line 215
14. lemma OAI.CoarseAssembly.mod_two_identity_first_pivot line 223
15. lemma OAI.CoarseAssembly.mod_two_identity_schur_pivot line 228
16. lemma OAI.CoarseAssembly.mod_two_kernel_mem_elementaryReduction line 239
17. theorem OAI.CoarseAssembly.elementaryReduction_surjective line 307

    Source documentation

    Surjectivity is proved by reduction to level one followed by elimination inside the kernel of reduction modulo two.

    theorem elementaryReduction_surjective (k : ℕ) : Function.Surjective (elementaryReduction k) := by
    …

    Mentions: OAI.CoarseAssembly.elementaryReduction