OAI/NumberTheory/PrimePackets/RootSubgroups.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.diag2n_decompose line 61
  2. theorem OAI.PrimeDegreePackets.specialLinear_transvection_induction line 79
  3. lemma OAI.PrimeDegreePackets.transvection_chain_commutator line 98
  4. lemma OAI.PrimeDegreePackets.root_subgroup_chain line 113
  5. def OAI.PrimeDegreePackets.invariantRightSubgroup line 129
  6. theorem OAI.PrimeDegreePackets.right_invariant_of_all_roots line 159
  7. lemma OAI.PrimeDegreePackets.diagonal_conjugation_transvection line 174
  8. lemma OAI.PrimeDegreePackets.root_mem_positive_reparameterize line 185
  9. lemma OAI.PrimeDegreePackets.root_mem_of_nonzero_parameter line 212
  10. def OAI.PrimeDegreePackets.rootInvarianceRelation line 236
  11. lemma OAI.PrimeDegreePackets.rootInvarianceRelation_trans line 240
  12. theorem OAI.PrimeDegreePackets.right_invariant_of_nontrivial_roots line 254
  13. lemma OAI.PrimeDegreePackets.observationEntropy_le_joint line 270
  14. lemma OAI.PrimeDegreePackets.observationEntropy_joint_eq_of_refines line 283
  15. lemma OAI.PrimeDegreePackets.observationEntropy_le_of_refines line 317
  16. lemma OAI.PrimeDegreePackets.orbitEntropy_one line 326
  17. lemma OAI.PrimeDegreePackets.orbitEntropy_le_mul line 334
  18. lemma OAI.PrimeDegreePackets.entropyRate_le_coding_error line 354
  19. lemma OAI.PrimeDegreePackets.observationEntropy_small_of_almost_constant line 391
  20. lemma OAI.PrimeDegreePackets.finite_compact_cores_separated line 426
  21. lemma OAI.PrimeDegreePackets.observationEntropyRate_eq_zero_of_isometry line 456
  22. lemma OAI.PrimeDegreePackets.measureEntropy_eq_zero_of_isometry line 557