mathlib
mathlib copied to clipboard
leanprover-community
Lean 3's obsolete mathematical components library: please use mathlib4
Some parts of the file use `[field R]`. This looks strange to me.
In the later PRs (#4297, #4430) for this series of definitions, I had suggestions that would apply equally to the previous files in the series (#4077, #4079, #4041). These should...
Quite often, the same group acts on the same space in many different ways. E.g., any group acts on itself in at least 3 different ways: `g • h =...
MWE: ```lean import tactic structure blah : Type := (f1 : ℕ) (f2 : ℕ) example : blah := begin refine_struct {..}, case f1 {}, /- Invalid `case`: there is...
wlog
It is nontrivial (currently for me impossible) to use `wlog` in the following example. ```lean lemma forty_two (a b c : ℕ) (h : (0:ℚ) < 1 - (1/a +...
Follow-up from #4771: > [we should redefine `tensor_product.map` to be [a] bundled hom. And `linear_map.tensor` can enable the notation `f.tensor g`.](https://github.com/leanprover-community/mathlib/pull/4771#discussion_r514983301) > Can we do anything to make that notation...
The following snippet triggers the "missing doc string" complaint from the linter: ```lean set_option old_structure_cmd true /-- Foo structure -/ structure foo := (x : ℕ) /-- Bar structure -/...
Proposed changes: * make `p` in `char_p` an `out_param`; * make it work for an `add_monoid` instead of a `semiring`; * use `char_p α 0` instead of `char_zero`. See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/char_zero.20and.20char_p)
Two useful results to have in mathlib are 1. the [Miracle Flatness Lemma](https://stacks.math.columbia.edu/tag/00R4), 2. [Zariski's Main Theorem](https://stacks.math.columbia.edu/tag/02LQ). Also, the Appendices of Bjorn Poonen's [Rational points on varieties](https://math.mit.edu/~poonen/papers/Qpoints.pdf), especially Appendix C...
Metadata
Owner
Metadata
Lean 3's obsolete mathematical components library: please use mathlib4