Commit 2022-05-11 23:41 9c54c410

View on Github →

feat: to_additive (#234) By @fpvandoorn. Depends on #129 Closes #229

Estimated changes

deleted theorem add_left_comm
deleted theorem add_right_comm
modified theorem inv_eq_of_mul_eq_one
modified theorem inv_inv
modified theorem inv_mul_cancel_left
modified theorem mul_inv_cancel_right
modified theorem mul_left_inj
modified theorem mul_left_inv
modified theorem mul_one
modified theorem mul_right_inj
modified theorem mul_right_inv
modified theorem one_mul
added def List.findIdx?
added def List.indexOf?
added def successIfFail
added structure Lean.NameMapAttribute
added structure Lean.NameMapAttributeImpl
added def Lean.toModifiers
added structure ToAdditive.ValueType
added theorem Test.bar0_works
added theorem Test.bar1_works
added theorem Test.bar2_works
added theorem Test.bar3_works
added theorem Test.bar7_works
added def Test.foo0
added def Test.foo1
added theorem Test.foo1_works
added def Test.foo2
added theorem Test.foo2_works
added def Test.foo3
added theorem Test.foo3_works
added def Test.foo4
added theorem Test.foo4_test
added def Test.foo5
added def Test.foo6
added def Test.foo7
added theorem Test.foo7_works
added def Test.foo_mul
added def Test.some_def