Commits leanprover-community/mathlib3

chore(linear_algebra/affine_space/affine_map): make `affine_map.coe_sub` true by definition (#10182)

ocfnash committed 4 years ago

8ac2fa06

refactor(measure_theory/integral/bochner): remove superfluous hypothesis (#10181)

fpvandoorn committed 4 years ago

b22a7c7e

feat(algebra/order/with_zero): add with_zero.linear_ordered_comm_grou… (#10180)

mariainesdff committed 4 years ago

88b4ce73

refactor(algebra/group): move `monoid.has_pow` etc to `algebra.group.defs` (#10147)

urkud committed 4 years ago

b31af6d9

feat(data/quot): add `quotient.lift₂_mk` (#10173)

shingtaklam1324 committed 4 years ago

16af388f

chore(data/bool): add `bool.lt_iff` (#10179)

urkud committed 4 years ago

35d36288

feat(measure_theory/covering/vitali_family): define Vitali families (#10057)

sgouezel committed 4 years ago

8991f28d

doc(group_theory/sylow): Expand Frattini's argument docstring (#10174)

tb65536 committed 4 years ago

6f9ec121

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

leanprover-community-bot committed 4 years ago

8490f2aa

feat(number_theory/lucas_primality): Add theorem for Lucas primality test (#8820)

BoltonBailey committed 4 years ago

41a820dd

feat(data/finset/prod): When `finset.product` is nonempty (#10170)

YaelDillies committed 4 years ago

d6a57f89

feat(data/fin/interval): Cardinality of `finset.Ixi`/`finset.Iix` in `fin` (#10168)

YaelDillies committed 4 years ago

b064622f

chore(topology/continuous_function/bounded): add simple lemmas (#10149)

urkud committed 4 years ago

fab61c9f

feat(algebra/group_with_zero/basic): relax some commutativity assumptions (#10075)

alexjbest committed 4 years ago

466fd276

feat(data/equiv/mul_add): add lemmas about multiplication and addition on a group being bijective and finite cancel_monoid_with_zeros (#10046)

alexjbest committed 4 years ago

ce0e0583

feat(analysis/ODE): prove Picard-Lindelöf/Cauchy-Lipschitz Theorem (#9791)

urkud committed 4 years ago

773a7a42

feat(topology/sheaves): Pullback of presheaf (#9961)

erdOne committed 4 years ago

74c27b25

chore(data/mv_polynomial/basic): add `map_alg_hom_coe_ring_hom` (#10158)

eric-wieser committed 4 years ago

79eb9344

chore(algebra/direct_sum/internal): add missing simp lemmas (#10154)

eric-wieser committed 4 years ago

11439d8c

feat(data/finset/interval): `finset α` is a locally finite order (#9963)

YaelDillies committed 4 years ago

828e1004

feat(group_theory/sylow): Sylow subgroups are nontrivial! (#10144)

tb65536 committed 4 years ago

cf2ff033

refactor(data/set/pairwise): Indexed sets as arguments to `set.pairwise_disjoint` (#9898)

YaelDillies committed 4 years ago

52cd4453

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