OAI/Algebra/Finitistic/Selection/TestModules.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.TestModule line 9
2. instance OAI.LittleFinitistic.testModule_nontrivial line 13
3. instance OAI.LittleFinitistic.testModule_finiteDimensional line 16
4. def OAI.LittleFinitistic.testRingMap line 20
5. instance OAI.LittleFinitistic.testModule_module line 24
6. theorem OAI.LittleFinitistic.testModule_smul_val line 28
7. instance OAI.LittleFinitistic.testModule_scalarTower line 32
8. theorem OAI.LittleFinitistic.testRingMap_algebraZ line 38
9. theorem OAI.LittleFinitistic.testModule_basis_action line 42
10. theorem OAI.LittleFinitistic.testModule_idempotent_action line 56

    Source documentation

    The first m−1 selecting idempotents act as identity; the next acts as zero.

    theorem testModule_idempotent_action (m : ℕ) [NeZero m] (i : Fin m) (x : TestModule m) :
        selectionIdempotent i.val • x = if i = lastIndex m then 0 else x := by
    …

    Mentions: OAI.LittleFinitistic.TestModule, OAI.LittleFinitistic.selectionIdempotent, OAI.LittleFinitistic.lastIndex