OAI/AlgebraicGeometry/SectionFields/TensorDomains.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Tensor domains over algebraically or relatively closed fields.

  1. theorem OAI.RelativeDenominators.finiteType_nonzero_specialization line 16
  2. def OAI.RelativeDenominators.tensorSubalgebraInclusion line 35
  3. lemma OAI.RelativeDenominators.tensorSubalgebraInclusion_transition line 39
  4. theorem OAI.RelativeDenominators.tensor_finiteType_field_of_definition line 49
  5. lemma OAI.RelativeDenominators.tensor_specialization_coordinate line 67
  6. theorem OAI.RelativeDenominators.tensor_domain_of_algClosed_finiteType line 82
  7. theorem OAI.RelativeDenominators.tensor_domain_of_algClosed line 129
  8. theorem OAI.RelativeDenominators.minpoly_map_of_relatively_closed line 169
  9. theorem OAI.RelativeDenominators.tensor_domain_of_relatively_closed_finite_separable line 184
  10. theorem OAI.RelativeDenominators.tensor_domain_of_finiteType_subalgebras line 209
  11. theorem OAI.RelativeDenominators.tensor_domain_of_relatively_closed_algebraic line 243
  12. theorem OAI.RelativeDenominators.tensor_domain_of_relatively_closed line 257