OAI/Algebra/AffineCancellation/Clearing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ComplexCancellation.Clearing.subalgebra line 11

   Source documentation

   Elements whose denominators can be cleared with a power of a fixed base element.

   def subalgebra (f : S →ₐ[k] R) (p : S) : Subalgebra k R where
   …

   Mentions: OAI.ComplexCancellation.p

2. lemma OAI.ComplexCancellation.Clearing.mem_base line 27
3. lemma OAI.ComplexCancellation.Clearing.injective_of_clearing line 29
4. lemma OAI.ComplexCancellation.Clearing.top_of_generators line 44