Commits leanprover-community/mathlib3

golf

jcommelin committed 4 years ago

17417621

feat(archive/imo): add formalised solution of IMO 1994 Q1

antoinelab01 committed 4 years ago

ac9db53f

feat(archive/imo): add formalised solution of IMO 1994 Q1

antoinelab01 committed 4 years ago

41ea82e3

feat(linear_algebra/affine_space/affine_map): decomposition of an affine map between modules as an equiv (#10162)

ocfnash committed 4 years ago

5187a427

chore(data/set): lemmas about `disjoint` (#10148)

urkud committed 4 years ago

22ec295c

split(data/finset/prod): split off `data.finset.basic` (#10142)

YaelDillies committed 4 years ago

69189d44

feat(ring_theory/polynomial/basic): `polynomial.ker_map_ring_hom` and `mv_polynomial.ker_map` (#10160)

eric-wieser committed 4 years ago

de79226c

chore(measure_theory/function/special_functions): import inner_product_space.basic instead of inner_product_space.calculus (#10159)

RemyDegenne committed 4 years ago

2129d053

chore(analysis/calculus/times_cont_diff): rename `linear_isometry_map.times_cont_diff`; drop `_map` (#10155)

ocfnash committed 4 years ago

b8908367

feat(linear_algebra/matrix/nonsingular_inverse): determinant of inverse is inverse of determinant (#10038)

eric-wieser committed 4 years ago

3cbe0feb

feat(topology/algebra/group_with_zero): continuity lemma for division (#9959)

fpvandoorn committed 4 years ago

17afc5c0

feat(data/nat/choose/basic): add some inequalities showing that choose is monotonic in the first argument (#10102)

alexjbest committed 4 years ago

211bdff0

feat(data/list): standardize list prefixes and suffixes (#10052)

EPronovost committed 4 years ago

1f0d878c

feat(topology/homotopy/basic): add `homotopic` for `continuous_map`s. (#9865)

shingtaklam1324 committed 4 years ago

4c0b6ada

chore(data/equiv/mul_add): DRY (#10150)

urkud committed 4 years ago

d219e6bb

chore(ring_theory/finiteness): make `finite_presentation.{quotient,mv_polynomial}` protected (#10091)

eric-wieser committed 4 years ago

76ba1b64

feat(algebra/group_power/order): Sign of an odd/even power without linearity (#10122)

YaelDillies committed 4 years ago

8658f40c

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

leanprover-community-bot committed 4 years ago

4770a6a7

refactor(analysis/calculus/mean_value): Remove useless hypotheses (#10129)

YaelDillies committed 4 years ago

0fac0807

refactor(algebra/direct_sum): rework internally-graded objects (#10127)

eric-wieser committed 4 years ago

fed57b54

feat(group_theory/sylow): Sylow subgroups are isomorphic (#10059)

tb65536 committed 4 years ago

6433c1c6

refactor(group_theory/complement): Introduce abbreviation for subgroups (#10009)

tb65536 committed 4 years ago

5541b256

chore(order/lattice): add `exists_lt_of_sup/inf` (#10133)

urkud committed 4 years ago

3a0b0d1d

chore(analysis/special_functions/trigonometric/inverse): move results about derivatives to a new file (#10110)

RemyDegenne committed 4 years ago

8f7ffec9

chore(logic/relation): rename to permit dot notation (#10105)

eric-wieser committed 4 years ago

00a1022f

feat(measure_theory/constructions/borel_space): decomposing the measure of a set into slices (#10096)

sgouezel committed 4 years ago

6993e6f8

feat(topology): properties about intervals and paths (#9914)

fpvandoorn committed 4 years ago

b51f18f7

feat(measure_theory/function/ae_measurable_order): an ae measurability criterion for ennreal-valued functions (#10072)

sgouezel committed 4 years ago

8d52be4a

feat(analysis/seminorm): define the Minkowski functional (#9097)

YaelDillies committed 4 years ago

4f033b7d

doc(linear_algebra): fix wrong docstring (#10139)

PatrickMassot committed 4 years ago

95cdebac