OAI/Algebra/FiniteTensor/KernelRelations.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Algebraic kernel relations, localization descent and polynomial parameter algebraicity.

  1. theorem OAI.PD4Tensor.Spreading.algebraic_kernel_annihilator line 16
  2. theorem OAI.PD4Tensor.Spreading.quotient_kernel_power_mem line 41
  3. theorem OAI.PD4Tensor.Spreading.quotient_mvpolynomial_isIntegral line 58
  4. theorem OAI.PD4Tensor.Spreading.diagonal_kernel_power_mem line 71
  5. theorem OAI.PD4Tensor.Spreading.localization_kernel_power_descent line 107
  6. theorem OAI.PD4Tensor.Spreading.nonmonic_diagonal_kernel_power_mem line 139
  7. theorem OAI.PD4Tensor.Spreading.diagonal_relation_det_ne_zero line 215
  8. theorem OAI.PD4Tensor.Spreading.exists_relation_derivative_ne_zero line 245
  9. theorem OAI.PD4Tensor.Spreading.polynomial_parameter_algebraicity line 279