leanprover-community/mathlib3

Pull Requests Commits

re-add support_mul_T

adomani committed 3 years ago

a9b5555f

Merge branch 'master' into adomani_degs_lp

adomani committed 3 years ago

040886f5

feat(measure_theory/measurable_space_def): add `generate_from_induction` (#15342)

RemyDegenne committed 3 years ago

2123bc38

feat(data/polynomial/laurent): define `degree` and some API (#15225)

adomani committed 3 years ago

0e72a4ed

refactor(algebra/algebra/subalgebra/basic): Remove `'` from `subalgebra.comap'` (#15349)

tb65536 committed 3 years ago

09a7f7a1

refactor(field_theory/*): Replace weaker `alg_hom.fintype` with stronger `alg_hom.fintype` (#15345)

tb65536 committed 3 years ago

8d749e60

feat(order/complete_boolean_algebra): A frame is distributive (#15340)

YaelDillies committed 3 years ago

b8b18fa5

chore(logic/equiv/basic): remove `nolint` (#15329)

vihdzp committed 3 years ago

11bfd9c9

feat(ring_theory/localization/basic): add `mk_sum` (#15261)

jjaassoonn committed 3 years ago

6f48d95d

doc(logic/equiv/basic): explicitly state functions equivalences are based on (#15354)

vihdzp committed 3 years ago

635b8585

feat(analysis/asymptotics/asymptotics): generalize, golf (#15010)

urkud committed 3 years ago

466b8922

golf(data/polynomial/degree/definitions): golf three proofs (#15236)

adomani committed 3 years ago

356f889c

feat(ring_theory/integrally_closed): if x is in Frac R such that x^n is in R then x is in R (#12812)

Multramate committed 3 years ago

0bea64b5

feat(data/fin/basic): add a reflected instance (#15337)

eric-wieser committed 3 years ago

f3fac409

chore(*): upgrade to lean 3.45.0c (#15325)

eric-wieser committed 3 years ago

48b7ad6f

feat(algebra/module/linear_map): use morphisms class for lemmas about linear [pre]images of `c • S` (#15103)

ADedecker committed 3 years ago

51f5e6cc

feat(measure_theory/integral/set_integral): add `set_integral_indicator` (#15344)

kex-y committed 3 years ago

25706131

feat(measure_theory/constructions/prod): The layercake integral. (#14424)

kkytola committed 3 years ago

f3ae2d0d

feat(ring_theory): Basic framework for classes of ring homomorphisms (#14966)

erdOne committed 3 years ago

073c3ace

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

leanprover-community-bot committed 3 years ago

e479bfbe

chore(set_theory/pgame): remove redundant `dsimp` (#15312)

vihdzp committed 3 years ago

b89df0ab

chore(data/matrix/block): lemmas about swapping blocks of matrices (#15298)

eric-wieser committed 3 years ago

4302cb7e

doc(set_theory/ordinal/cantor_normal_form): document most theorems (#15227)

vihdzp committed 3 years ago

5590b0a2

chore(order/order_iso_nat): remove `decidable_pred` assumption from `subtype.order_iso_of_nat` (#15190)

vihdzp committed 3 years ago

5744b50d

feat(data/finset/basic): Add `decidable_nonempty` for finsets. (#15170)

linesthatinterlace committed 3 years ago

08648056

feat(linear_algebra/projectivization/independence): defines (in)dependence of points in projective space (#14542)

Michael14071407 committed 3 years ago

1e82f5ec

feat(topology/local_homeomorph): "injectivity" local_homeomorph.prod (#15311)

fpvandoorn committed 3 years ago

f7313156

feat(analysis/calculus/cont_diff): extra lemmas about cont_diff_within_at (#15309)

fpvandoorn committed 3 years ago

25f60b46

feat(tactic/linear_combination): add parser for `h / a` (#15284)

digama0 committed 3 years ago

51f76d05

feat(topology/algebra/order): ⁻¹ continuous for linear ordered fields (#15022)

ericrbg committed 3 years ago

be53c7cb

Older