OAI/Analysis/GroupDeterminants/TraceLog.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GroupRingDeterminant.hasDerivAt_trace_log_one_sub line 17
  2. lemma OAI.GroupRingDeterminant.log_smul_of_isUnit line 32
  3. lemma OAI.GroupRingDeterminant.norm_one_sub_rescale_star_mul_self line 57
  4. lemma OAI.GroupRingDeterminant.ringInverse_smul line 88
  5. lemma OAI.GroupRingDeterminant.hasDerivAt_trace_log_of_rescale line 100
  6. lemma OAI.GroupRingDeterminant.trace_star_mul_self_log_derivative_value line 136
  7. lemma OAI.GroupRingDeterminant.hasDerivAt_trace_log_star_mul_self line 153
  8. lemma OAI.GroupRingDeterminant.trace_derivative_mul_value line 171
  9. def OAI.GroupRingDeterminant.nilpotentShearUnit line 183
  10. lemma OAI.GroupRingDeterminant.ringInverse_nilpotentShear line 194
  11. lemma OAI.GroupRingDeterminant.nilpotentShear_trace_derivative line 199
  12. lemma OAI.GroupRingDeterminant.trace_log_shear_invariant line 205