Commit 2020-02-07 06:21 f912a6b4

View on Github →

feat(algebraic_geometry/prime_spectrum): first definitions (#1957)

Start on prime spectrum
Define comap betwee prime spectra; prove continuity
Update src/algebraic_geometry/prime_spectrum.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
chore(*): rename filter.inhabited_of_mem_sets to nonempty_of_mem_sets (#1943) In other names inhabited means that we have a default element.
refactor(linear_algebra/multilinear): cleanup of multilinear maps (#1921)
staging [ci skip]
staging
staging
cleanup norms
complete currying
docstrings
docstrings
cleanup
nonterminal simp
golf
missing bits for derivatives
sub_apply
cleanup
better docstrings
remove two files
reviewer's comments
use fintype
line too long
feat(ring_theory/power_series): several simp lemmas (#1945)
Small start on generating functions
Playing with Bernoulli
Finished sum_bernoulli
Some updates after PRs
Analogue for mv_power_series
Cleanup after merged PRs
feat(ring_theory/power_series): several simp lemmas
Remove file that shouldn't be there yet
Update src/ring_theory/power_series.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
Generalise lemma to canonically_ordered_monoid
Update name
Fix build
feat(tactic/lint): Three new linters, update illegal_constants (#1947)
add three new linters
fix failing declarations
restrict and rename illegal_constants linter
update doc
update ge_or_gt test
update mk_nolint
fix error
Update scripts/mk_nolint.lean Co-Authored-By: Rob Lewis Rob.y.lewis@gmail.com
Update src/meta/expr.lean Co-Authored-By: Rob Lewis Rob.y.lewis@gmail.com
clarify unfolds_to_class
fix names since name is no longer protected also change one declaration back to instance, since it did not cause a linter failure
fix errors, move notes to docstrings
add comments to docstring
update mk_all.sh
fix linter errors
feat(number_theory/bernoulli): Add definition of Bernoulli numbers (#1952)
Small start on generating functions
Playing with Bernoulli
Finished sum_bernoulli
Some updates after PRs
Analogue for mv_power_series
Cleanup after merged PRs
feat(number_theory/bernoulli): Add definition of Bernoulli numbers
Remove old file
Process comments
feat(topology/algebra/multilinear): define continuous multilinear maps (#1948)
feat(data/set/intervals): define intervals and prove basic properties (#1949)
things about intervals
better documentation
better file name
add segment_eq_interval
better proof for is_measurable_interval
better import and better proof
better proof
refactor(*): migrate from ≠ ∅ to set.nonempty (#1954)
refactor(*): migrate from ≠ ∅ to set.nonempty Sorry for a huge PR but it's easier to do it in one go. Basically, I got rid of all ≠ ∅ in theorem/def types, then fixed compile. I also removed most lemmas about ≠ ∅ from set/basic to make sure that I didn't miss something I should change elsewhere. Should I restore (some of) them?
Fix compile of archive/
Drop +1 unneeded argument, thanks @sgouezel.
Fix build
Update src/algebraic_geometry/prime_spectrum.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
Update src/algebraic_geometry/prime_spectrum.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
Change I to s, and little fixes
Update src/algebraic_geometry/prime_spectrum.lean Co-Authored-By: Chris Hughes 33847686+ChrisHughes24@users.noreply.github.com
Update src/algebraic_geometry/prime_spectrum.lean Co-Authored-By: Chris Hughes 33847686+ChrisHughes24@users.noreply.github.com
Update src/algebraic_geometry/prime_spectrum.lean Co-Authored-By: Chris Hughes 33847686+ChrisHughes24@users.noreply.github.com
Update src/algebraic_geometry/prime_spectrum.lean Co-Authored-By: Chris Hughes 33847686+ChrisHughes24@users.noreply.github.com
Indentation
Update prime_spectrum.lean
fix build