Commits leanprover-community/mathlib

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

feat(analysis/normed_space): a normed space over a nondiscrete normed field is noncompact (#10994)

urkud committed 4 years ago

f03447fb

feat(analysis/mean_inequalities): Minkowski inequality for infinite sums (#10984)

hrmacbeth committed 4 years ago

0ac9f83b

chore(topology/metric_space): export `is_compact_closed_ball` (#10973)

urkud committed 4 years ago

1a780f69

feat(algebraic_geometry): Define `open_cover`s of Schemes. (#10931)

erdOne committed 4 years ago

36ba1acd

feat(data/nat/nth): add nth function (#10707)

BoltonBailey committed 4 years ago

c374a3b9

feat(algebraic_topology): alternating face map complex of a simplicial object (#10927)

joelriou committed 4 years ago

421b9bbe

feat(logic/basic): When a dependent If-Then-Else is not one of its arguments (#10924)

YaelDillies committed 4 years ago

dc57de22

feat(group_theory/submonoid/membership): upgrade definition of pow from a set morphism to a monoid morphism (#10898)

apurvnakade committed 4 years ago

1db0052e

feat(algebra/algebra/spectrum): prove the spectral mapping theorem for polynomials (#10783)

j-loreaux committed 4 years ago

68aada0d

feat(data/rat/basic): API around rat.mk (#10782)

pechersky committed 4 years ago

720fa8fa

feat(data/real/sqrt): add a few lemmas (#11003)

urkud committed 4 years ago

4ce0d047

chore(measure_theory): golf a proof (#11002)

urkud committed 4 years ago

694b3f85

refactor(analysis/seminorm): Weaken typeclasses (#10999)

YaelDillies committed 4 years ago

3362b1e2