OAI/Computability/RationalHitting/BlockDivision.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RationalHitting.PolynomialHahn.Exponents line 9
  2. def OAI.RationalHitting.PolynomialHahn.exponent line 12
  3. lemma OAI.RationalHitting.PolynomialHahn.exponent_injective line 14
  4. def OAI.RationalHitting.PolynomialHahn.variableSeries line 22
  5. def OAI.RationalHitting.PolynomialHahn.embed line 25
  6. lemma OAI.RationalHitting.PolynomialHahn.embed_monomial line 28
  7. lemma OAI.RationalHitting.PolynomialHahn.embed_coeff line 38
  8. lemma OAI.RationalHitting.PolynomialHahn.embed_injective line 50
  9. def OAI.RationalHitting.BlockDivision.blockEmbedding line 67
  10. lemma OAI.RationalHitting.BlockDivision.unit_of_vecMul_injective line 86
  11. def OAI.RationalHitting.BlockDivision.kernelRows line 110

    Source documentation

    A nonzero row of a division-ring kernel expands into d independent ordinary kernel rows after a faithful d-dimensional representation.

    def kernelRows (φ : D →+* Matrix (κ) (κ) E) (v : m → D) :
    (κ → E) →ₗ[E] (m × κ → E) where
…
  12. lemma OAI.RationalHitting.BlockDivision.kernelRows_injective line 116
  13. lemma OAI.RationalHitting.BlockDivision.kernelRows_mem line 130
  14. theorem OAI.RationalHitting.BlockDivision.rank_gap line 153

    Source documentation

    The rank gap obtained by block elimination over a division ring.

    theorem rank_gap (φ : D →+* Matrix (κ) (κ) E)
    (A : Matrix (m) (m) D) :
    IsUnit (blockEmbedding φ A) ∨ (blockEmbedding φ A).rank + Fintype.card κ ≤ Fintype.card m * Fintype.card κ := by
…

    Mentions: OAI.RationalHitting.BlockDivision.blockEmbedding

  15. theorem OAI.RationalHitting.BlockDivision.isUnit_of_rank_gt line 181
  16. theorem OAI.RationalHitting.RankSpecialization.rank_le line 205

    Source documentation

    Specialization cannot raise the generic rank. This version requires no unstated minor criterion: a rank normal form supplies a nonzero minor after constant row and column changes.

    theorem rank_le (ev : P →ₐ[K] K) (inclusion : P →+* E)
    (hinj : Function.Injective inclusion) (A : Matrix ι ι P) :
    (ev.toRingHom.mapMatrix A).rank ≤ (inclusion.mapMatrix A).rank := by
…