OAI/LinearAlgebra/TensorProduct/ScalarDescent.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Tensor scalar descent over finite and arbitrary Galois extensions.

  1. theorem OAI.RationalHodgeCM.Partial.one_tmul_mem_baseChange_iff line 19
  2. theorem OAI.RationalHodgeCM.Partial.comap_baseChange line 31
  3. def OAI.RationalHodgeCM.Partial.scalarConjugate line 43
  4. theorem OAI.RationalHodgeCM.Partial.scalarConjugate_tmul line 47
  5. theorem OAI.RationalHodgeCM.Partial.scalarConjugate_smul line 50
  6. def OAI.RationalHodgeCM.Partial.tensorTrace line 56
  7. theorem OAI.RationalHodgeCM.Partial.tensorTrace_tmul line 60
  8. theorem OAI.RationalHodgeCM.Partial.one_tmul_tensorTrace line 65
  9. def OAI.RationalHodgeCM.Partial.rationalPart line 74
  10. theorem OAI.RationalHodgeCM.Partial.mem_rationalPart line 79
  11. theorem OAI.RationalHodgeCM.Partial.tensorTrace_traceDual_smul line 82
  12. theorem OAI.RationalHodgeCM.Partial.finite_galois_scalar_descent line 95
  13. def OAI.RationalHodgeCM.Partial.coefficientInclusion line 119
  14. theorem OAI.RationalHodgeCM.Partial.coefficientInclusion_tmul line 123
  15. theorem OAI.RationalHodgeCM.Partial.coefficientInclusion_mem_baseChange line 126
  16. theorem OAI.RationalHodgeCM.Partial.rationalPart_comap_coefficientInclusion line 135
  17. theorem OAI.RationalHodgeCM.Partial.tensor_defined_over_finite_galois line 148
  18. theorem OAI.RationalHodgeCM.Partial.scalarConjugate_restrict line 163
  19. theorem OAI.RationalHodgeCM.Partial.galois_scalar_descent line 173
  20. theorem OAI.RationalHodgeCM.Partial.scalar_descent_ambient line 200
  21. abbrev OAI.RationalHodgeCM.Partial.AlgebraicNumbers line 211
  22. theorem OAI.RationalHodgeCM.Partial.trace_descent line 213