OAI/Probability/SignedSweeps/InjectionRestriction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.irreducible_comp_surjective line 10
2. lemma OAI.SignedSweeps.coefficientAction_comp_equiv line 44
3. lemma OAI.SignedSweeps.restrictionEligible_range_iff line 53
4. theorem OAI.SignedSweeps.positive_injective_restriction line 88
5. lemma OAI.SignedSweeps.viaEmbeddingHom_injective line 122