OAI/RingTheory/BassTrace/TraceCoefficients.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BassTrace.classCoefficient line 9

    Distinct definitions of this name: ComparatorChallenges/BassTorsionFree.lean:11 (same statement text; different proof or body), ComparatorChallenges/BassTrace.lean:19 (same declaration text). Qualify references as OAI.BassTrace.classCoefficient@path.

  2. def OAI.BassTrace.idempotentTraceCoefficient line 14
  3. theorem OAI.BassTrace.classCoefficient_zero line 20

    Also declared: ComparatorChallenges/BassTorsionFree.lean:18 (same declaration text).

  4. theorem OAI.BassTrace.classCoefficient_single line 24

    Also declared: ComparatorChallenges/BassTorsionFree.lean:22 (same declaration text).

  5. theorem OAI.BassTrace.classCoefficient_add line 29

    Also declared: ComparatorChallenges/BassTorsionFree.lean:27 (same declaration text).

  6. theorem OAI.BassTrace.classCoefficient_smul line 38

    Also declared: ComparatorChallenges/BassTorsionFree.lean:36 (same declaration text).

  7. theorem OAI.BassTrace.classCoefficient_sum line 48

    Also declared: ComparatorChallenges/BassTorsionFree.lean:46 (same declaration text).

  8. theorem OAI.BassTrace.classCoefficient_mul_comm line 56

    Also declared: ComparatorChallenges/BassTorsionFree.lean:54 (same declaration text).

  9. theorem OAI.BassTrace.classCoefficient_matrix_mul_comm line 75

    Also declared: ComparatorChallenges/BassTorsionFree.lean:73 (same declaration text).