Commits leanprover-community/mathlib

chore(algebra/group): move is_unit.inv lemmas (#9364)

pechersky committed 4 years ago

b0cd1f9c

chore(data/pi): add missing `pi.{inv,neg}_def` (#9361)

eric-wieser committed 4 years ago

c42aaa3d

feat(group_theory/*/pointwise): Copy set lemmas about pointwise actions to subgroups and submonoids (#9359)

eric-wieser committed 4 years ago

8ff756cb

chore(measure_theory/integral/interval_integral): generalize `integral_smul` (#9355)

urkud committed 4 years ago

18f06ecf

chore(linear_algebra/basic): add `linear_map.neg_comp`, generalize `linear_map.{sub,smul}_comp` (#9335)

eric-wieser committed 4 years ago

7cb72461

chore(linear_algebra/basic): split out quotients and isomorphism theorems (#9332)

kim-em committed 4 years ago

c794c5c8

feat(data/dfinsupp): add submodule.bsupr_eq_range_dfinsupp_lsum (#9202)

eric-wieser committed 4 years ago

6f2d1ba2

chore(*): remove some `assume`s (#9365)

ericrbg committed 4 years ago

981f8baa

feat(measure_theory/function/conditional_expectation): define the conditional expectation of a function, prove the equality of integrals (#9114)

RemyDegenne committed 4 years ago

e14cf589

feat(linear_algebra/affine_space/affine_map): add missing simp lemma `affine_map.homothety_apply_same` (#9360)

ocfnash committed 4 years ago

0db6caf8

chore(algebra/basic): split out facts about lmul (#9300)

kim-em committed 4 years ago

48883dcd

refactor(measure_theory/measure/regular): add `inner_regular`, `outer_regular`, generalize (#9283)

urkud committed 4 years ago

854e5c6b

feat(linear_algebra/free_modules): add instances (#9223)

riccardobrasca committed 4 years ago

a512db14

feat(measure_theory): `ι → α ≃ᵐ α` if `[unique ι]` (#9353)

urkud committed 4 years ago

6a9ba186

feat(category_theory/opposites): Add is_iso_op (#9319)

justus-springer committed 4 years ago

9e59e291

feat(algebra,group_theory): smul_(g)pow (#9311)

pechersky committed 4 years ago

9618d73c

feat(linear_algebra): redefine `linear_map` and `linear_equiv` to be semilinear (#9272)

dupuisf committed 4 years ago

a9cd8c25

Merge branch 'master' of https://github.com/leanprover-community/mathlib into affine_schemes

erdOne committed 4 years ago

c9ab14b3

feat(ring_theory/localization): Localizing at units is isomorphic to the ring (#9324)

erdOne committed 4 years ago

a7a9c91e

chore(linear_algebra): rename endomorphism multiplicative structures for consistency (#9336)

eric-wieser committed 4 years ago

4a8fb6a3

chore(*): linting (#9342)

kim-em committed 4 years ago

dd519dfa

feat(algebra/*): Tensor product is the fibered coproduct in CommRing (#9338)

erdOne committed 4 years ago

1a341fd8

feat(measure_theory/integral/*): integral over map (e : α ≃ᵐ β) μ (#9316)

urkud committed 4 years ago

2d17f521

feat(measure_theory/measure/measure_space): add measure_Union_of_null_inter (#9307)

alexjbest committed 4 years ago

18f0093f

feat(ring_theory/derivation): helper lemma for custom `derivation_ext` lemmas (#9255)

urkud committed 4 years ago

7e3256ba

feat(topology/compact_open): convergence in the compact-open topology can be checked on compact sets (#9240)

hrmacbeth committed 4 years ago

9b1f0bb6

feat(algebra/pointwise): more to_additive attributes for new lemmas (#9348)

alexjbest committed 4 years ago

d2f7b24d

feat(data/fintype/basic): embeddings of fintypes based on cardinal inequalities (#9346)

sgouezel committed 4 years ago

88c79e57

feat(analysis/calculus/[f]deriv): derivative of pointwise composition/application of continuous linear maps (#9174)

ADedecker committed 4 years ago

c950c45e

chore(analysis/normed_space/conformal_linear_map): delay dependence on inner products (#9293)

kim-em committed 4 years ago

54eb6037