OAI/Analysis/Kaplansky/Quotient/NullIdeal.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KaplanskyConsequences.Mat line 15
  2. abbrev OAI.KaplanskyConsequences.SpectralKernel.val line 27
  3. lemma OAI.KaplanskyConsequences.SpectralKernel.val_of_nonneg line 29
  4. lemma OAI.KaplanskyConsequences.SpectralKernel.val_zero line 33
  5. lemma OAI.KaplanskyConsequences.SpectralKernel.val_nonneg line 35
  6. lemma OAI.KaplanskyConsequences.SpectralKernel.val_mono line 39
  7. lemma OAI.KaplanskyConsequences.SpectralKernel.val_one line 44
  8. lemma OAI.KaplanskyConsequences.SpectralKernel.val_smul line 48
  9. lemma OAI.KaplanskyConsequences.SpectralKernel.val_shift line 51
  10. lemma OAI.KaplanskyConsequences.SpectralKernel.val_square_swap line 56
  11. lemma OAI.KaplanskyConsequences.SpectralKernel.abs_val_sub_le line 61
  12. lemma OAI.KaplanskyConsequences.SpectralKernel.mat_sum_apply line 66
  13. lemma OAI.KaplanskyConsequences.SpectralKernel.gram_nonneg line 73
  14. lemma OAI.KaplanskyConsequences.SpectralKernel.gram_swap line 94
  15. lemma OAI.KaplanskyConsequences.SpectralKernel.weighted_gram_identity line 102
  16. lemma OAI.KaplanskyConsequences.SpectralKernel.val_add_le line 132
  17. lemma OAI.KaplanskyConsequences.SpectralKernel.val_add_of_zero line 183
  18. abbrev OAI.KaplanskyConsequences.SpectralKernel.IsNull line 198
  19. lemma OAI.KaplanskyConsequences.SpectralKernel.null_zero line 200
  20. lemma OAI.KaplanskyConsequences.SpectralKernel.null_star line 202
  21. lemma OAI.KaplanskyConsequences.SpectralKernel.null_add line 205
  22. lemma OAI.KaplanskyConsequences.SpectralKernel.null_smul line 220
  23. lemma OAI.KaplanskyConsequences.SpectralKernel.null_mul_left line 230
  24. lemma OAI.KaplanskyConsequences.SpectralKernel.null_mul_right line 244
  25. lemma OAI.KaplanskyConsequences.SpectralKernel.continuous_squareVal line 248
  26. def OAI.KaplanskyConsequences.SpectralKernel.nullIdeal line 255
  27. lemma OAI.KaplanskyConsequences.SpectralKernel.val_zero_of_null line 266
  28. lemma OAI.KaplanskyConsequences.SpectralKernel.null_of_val_zero line 275
  29. lemma OAI.KaplanskyConsequences.SpectralKernel.null_posPart line 282
  30. lemma OAI.KaplanskyConsequences.SpectralKernel.null_sub line 286
  31. lemma OAI.KaplanskyConsequences.SpectralKernel.val_eq_of_null_sub line 289
  32. lemma OAI.KaplanskyConsequences.SpectralKernel.val_scalar_sub line 304