Jujian Zhang
Jujian Zhang
There is a weird issue: if I put instances like `set_like \sigma A` etc inside `def`/`lemma`, then Lean can find them, but if I put them in `variables`, then Lean...
This works, thanks > You probably need an `include \sigma` line to make lean aware that you intend to refer to `\sigma`
@eric-wieser, this PR has been forgotten by me and you. Could you please have a look again please. Thanks.
> What's the difference between `module ℚ A` and `divisible A`? Is the following true? > > ```lean > /-- Any rat-module is divisible -/ > def divisible_of_rat_module [module ℚ...
> I think we might want a multiplicative group version of this too? with the one here generated by to_additive? Certainly there are nice examples like algebraically closed fields that...
> I also think this notion could be more useful when defined for `comm_monoid`s, so we cover groups_with_zero too, (such as fields again), the property of nat divisibility implies int...
> Is there a reason why [doc#tensor_product.left_module](https://leanprover-community.github.io/mathlib_docs/linear_algebra/tensor_product.html#tensor_product.left_module) is not used? Maybe I am missing something, but to use `tensor_product.left_module`, `M` needs to be an `S`-module where it is an `R`-module?
If needed, I will split this PR further
> With these golfs, I think it's good to go once #16083 is merged. Thanks! Thank you so much for taking the time to golf all these long and poorly...
This PR originally started as defining skyscraper sheaf, but now too many things has been added, so I will move the definition of skyscraper sheaf into another branch (#15934).