OAI/Topology/ArtinGroups/Complexes/Subrepresentation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.CoefficientArrays.IsSubrepresentation line 10
2. def OAI.HarmonicArtin.CoefficientArrays.socle line 14
3. theorem OAI.HarmonicArtin.CoefficientArrays.mem_socle line 18
4. theorem OAI.HarmonicArtin.CoefficientArrays.exists_nonzero_socle line 22
5. theorem OAI.HarmonicArtin.CoefficientArrays.subrepresentation_eq_bot_of_socle_eq_bot line 46
6. theorem OAI.HarmonicArtin.CoefficientArrays.range_isSubrepresentation line 68
7. theorem OAI.HarmonicArtin.CoefficientArrays.map_eq_zero_of_socle_eq_bot line 78