Commits leanprover-community/mathlib3

Merge branch 'master' into dupuisf/self_adjoint

dupuisf committed 4 years ago

570efd53

chore(algebraic_geometry): Remove unwanted spaces. (#11042)

erdOne committed 4 years ago

aa669096

feat(data/mv_polynomial): API for mv polynomial.rename (#10921)

isadofschi committed 4 years ago

d6ecc14a

feat(analysis/inner_product_space/adjoint): show that continuous linear maps on a Hilbert space form a C*-algebra (#10837)

dupuisf committed 4 years ago

f7038c24

feat(combinatorics/configuration): Inequality between `point_count` and `line_count` (#11036)

tb65536 committed 4 years ago

8a997f3f

feat(measure_theory/covering/besicovitch): covering a set by balls with controlled measure (#11035)

sgouezel committed 4 years ago

8181fe89

refactor(data/nat/prime): redefine nat.prime as irreducible (#11031)

Ruben-VandeVelde committed 4 years ago

a998db66

feat(data/multiset/basic): empty_or_exists_mem (#11023)

ericrbg committed 4 years ago

3588c3a0

chore(ring_theory/adjoin/power_basis): add `simps` (#11018)

ericrbg committed 4 years ago

404a9125

feat(ring_theory/derivation): add 3 lemmas (#10996)

urkud committed 4 years ago

d5a3e8c2

feat(topology,analysis): there exists `y ∈ frontier s` at distance `inf_dist x sᶜ` from `x` (#10976)

urkud committed 4 years ago

c4268a86

chore(topology/*): Eliminate `finish` (#10991)

stuart-presnell committed 4 years ago

5dac1c08

feat(algebra/order/field, data/real/basic): lemmas about `Sup` and `is_lub` (#11013)

hrmacbeth committed 4 years ago

35b67fd9

feat(analysis/inner_product_space/adjoint): define the adjoint of a continuous linear map between Hilbert spaces (#10825)

dupuisf committed 4 years ago

3377bccd

feat(analysis/normed_space/spectrum): adds easy direction of Gelfand's formula for the spectral radius (#10847)

j-loreaux committed 4 years ago

99c634cc

chore(group_theory/quotient_group): change injective_ker_lift to ker_lift_injective for naming regularisation (#11027)

Multramate committed 4 years ago

ffbab0dc

feat(combinatorics/configuration): Sum of line counts equals sum of point counts (#11026)

tb65536 committed 4 years ago

a0993e4d

feat(data/polynomial/ring_division): roots.le_of_dvd (#11025)

ericrbg committed 4 years ago

04aeb019

feat(combinatorics/configuration): `nondegenerate.exists_injective_of_card_le` (#11019)

tb65536 committed 4 years ago

c0e613a2

feat(data/real/ennreal): trichotomy lemmas (#11014)

hrmacbeth committed 4 years ago

2c4e6dfd

feat(field_theory/adjoin): lemmas about `inf`s of `intermediate_field`s (#10997)

eric-wieser committed 4 years ago

7c7195f6

feat(combinatorics/simple_graph/connectivity): walks, paths, cycles (#10981)

kmill committed 4 years ago

d329d6bd

feat(topology/is_locally_homeomorph): New file (#10960)

tb65536 committed 4 years ago

028c161c

feat(field_theory/adjoin): Supremum of finite dimensional intermediate fields (#10938)

tb65536 committed 4 years ago

a0f12bc1

feat(group_theory/specific_groups/cyclic): |G|=expG ↔ G is cyclic (#10692)

ericrbg committed 4 years ago

084b1ac2

feat(topology/connected): add `inducing.is_preconnected_image` (#11011)

urkud committed 4 years ago

6c6c7da8

chore(scripts): update nolints.txt (#11028)

leanprover-community-bot committed 4 years ago

67cf4061

feat(algebra/pointwise): expand API for multiplication / addition of finsets by copying the corresponding API for sets (#10600)

alexjbest committed 4 years ago

f846a426

chore(number_theory/primorial): golf some proofs (#11024)

Ruben-VandeVelde committed 4 years ago

7b641cba

feat(ring_theory/derivation): drop unused `is_scalar_tower` (#10995)

urkud committed 4 years ago

1dd60802