OAI/Computability/RationalHitting/Evaluation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RationalHitting.Formula.Eval.unique line 10
2. lemma OAI.RationalHitting.Formula.Eval.map line 29
3. lemma OAI.RationalHitting.Formula.Eval.lift line 42

   Source documentation

   Defined evaluations lift through a homomorphism reflecting units. In particular this handles every inverse occurrence before considering the root.

   lemma Eval.lift (f : R →+* S) (hf : ∀ x, IsUnit (f x) → IsUnit x)
       {c : ℚ →+* R} {X : Fin n → R} {h : Formula n} {a : S}
       (ha : Eval (f.comp c) (fun i => f (X i)) h a) :
       ∃ b : R, Eval c X h b ∧ f b = a := by
   …

   Mentions: OAI.RationalHitting.Formula, OAI.RationalHitting.Formula.Eval

4. lemma OAI.RationalHitting.Formula.Eval.unit_of_division_lift line 68

   Source documentation

   Mapping a defined nonzero value out of a division ring makes it a unit. This is used after the partial-specialization domain proof, not instead of it.

   lemma Eval.unit_of_division_lift {D : Type*} [DivisionRing D] [Nontrivial R]
       (f : D →+* R) {c : ℚ →+* D} {X : Fin n → D} {h : Formula n} {a : R}
       (ha : Eval (f.comp c) (fun i => f (X i)) h a) (ha0 : a ≠ 0) : IsUnit a := by
   …

   Mentions: OAI.RationalHitting.Formula, OAI.RationalHitting.Formula.Eval

5. abbrev OAI.RationalHitting.NoncommBlocks.matMul line 89
6. lemma OAI.RationalHitting.NoncommBlocks.upper_unit line 92
7. lemma OAI.RationalHitting.NoncommBlocks.lower_unit line 97
8. lemma OAI.RationalHitting.NoncommBlocks.diag_unit_iff line 102
9. lemma OAI.RationalHitting.NoncommBlocks.schur_factor line 135
10. lemma OAI.RationalHitting.NoncommBlocks.schur_unit_iff line 145
11. lemma OAI.RationalHitting.NoncommBlocks.schur_inverse line 157