Yury G. Kudryashov
Yury G. Kudryashov
@johoelzl Could you please explain what does `src/tactic/transfer` do?
Can it do all the transfers in `data/equiv/transfer_instance`? Does it produce the same definitional equalities?
@sgouezel Do I understand correctly that this will be a part of your project on formalizing analytic functions?
@101damnations what's the status of your rewrite of `localization`?
@jcommelin We can use something like `g •[a] x`, and leave `g • x` to (semi-)modules scalar multiplication. If some file deals with only one group action, you can always...
@ChrisHughes24 I thought that classes are mostly for “canonical” structures. I mean, as soon as you want to deal with specific actions instead of abstract ones, in many cases you...
@rwbarton It seems that we have very different examples in mind. For me (as a dynamical systems person), it is very common to have, e.g., `multiplicative int` acting on some...
Started in https://github.com/leanprover-community/mathlib/tree/mul_action
I wrote most comments here when I knew much less about `mathlib`. Now I think that we should have a `structure` and lemmas that take a `structure` argument in the...
We should skip constructors of inductive types as well (at least, for now).