OAI/Combinatorics/Chromatic/GradedAlgebra/TraceLogDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.FormalLog.trace_log_derivative line 14
2. lemma OAI.ElementaryPositivity.FormalLog.inverse_product line 44
3. lemma OAI.ElementaryPositivity.FormalLog.trace_log_product line 54