leanprover-community/mathlib3

Pull Requests Commits

Update lemmas.lean

eric-wieser committed 4 years ago

Verified 510adc49

feat(algebra/group_power/lemmas): remove commutativity requirement from `is_unit_pos_pow_iff`

eric-wieser committed 4 years ago

Verified 702cfc17

feat(category_theory/limits/shapes/images): some explicit instances of has_image_map (#9977)

jcommelin committed 4 years ago

e1bafaa4

feat(measure_theory/group/arithmetic): add a section about `opposite` (#10026)

urkud committed 4 years ago

4f3443a8

fix(tactic/norm_cast): make push_cast discharger match the others (#10021)

robertylewis committed 4 years ago

3f6174ba

chore(algebra/module/submodule_lattice): lemmas about the trivial submodule (#10022)

hrmacbeth committed 4 years ago

4ce2a5f1

feat(data/list/defs): map_with_prefix_suffix and map_with_complement (#10020)

robertylewis committed 4 years ago

7538f9b4

chore(measure_theory): drop a few `measurable_set` assumptions (#9999)

urkud committed 4 years ago

c7f51395

feat(linear_algebra/matrix/adjugate): det_adjugate and adjugate_adjugate (#9991)

eric-wieser committed 4 years ago

bdcb7310

chore(topology,measure_theory): generalize a few instances (#9967)

urkud committed 4 years ago

415da222

feat(archive/imo): IMO 2021 Q1 (#8432)

MantasBaksys committed 4 years ago

0cfae438

feat(ring_theory/adjoin_root): golf and generalize the algebra structure on `adjoin_root` (#10019)

eric-wieser committed 4 years ago

99a2d5bf

feat(data/finset/interval): Bounded intervals in locally finite orders are finite (#9960)

YaelDillies committed 4 years ago

18dce134

feat(list): add some lemmas (#9873)

EPronovost committed 4 years ago

17339204

feat(data/set/function): restrict `dite/ite/piecewise/extend` (#10017)

urkud committed 4 years ago

e927aa4e

chore(*): a few lemmas about `range_splitting (#10016)

urkud committed 4 years ago

0d6548fc

chore(measure_theory/measure/measure_space): reorder, golf (#10015)

urkud committed 4 years ago

b9ff26b5

feat(order/bounded_lattice): add `is_compl.le_sup_right_iff_inf_left_le` (#10014)

urkud committed 4 years ago

fd6f6816

fix(field_theory/intermediate_field): use a better `algebra.smul` definition, and generalize (#10012)

eric-wieser committed 4 years ago

22d32dcd

feat(group_theory/subgroup/basic): `mul_mem_sup` (#10007)

tb65536 committed 4 years ago

fe76b5c0

move(data/set/pairwise): Move `set.pairwise_on` (#9986)

YaelDillies committed 4 years ago

c495ed61

feat(computability/tm_to_partrec): prove finiteness (#6955)

digama0 committed 4 years ago

628f418d

feat(data/{finset,multiset}/locally_finite): Simple interval lemmas (#9877)

YaelDillies committed 4 years ago

c8d14294

feat(analysis/normed_space/pi_Lp): use typeclass inference for `1 ≤ p` (#9922)

hrmacbeth committed 4 years ago

acbb2a53

chore(measure_theory): a `continuous_map` is measurable (#9998)

urkud committed 4 years ago

b0349aa9

feat(measure/measurable_space): add `measurable_equiv.of_unique_of_unique` (#9968)

urkud committed 4 years ago

73423cf9

feat(analysis/inner_product_space/dual): complex Riesz representation theorem (#9924)

hrmacbeth committed 4 years ago

7f2b8064

feat(category_theory/arrow): is_iso, mono, epi instances for maps between arrows (#9976)

jcommelin committed 4 years ago

f78b7398

feat(measure_theory/construction/borel_space): two measures are equal if they agree on closed-open intervals (#9396)

kex-y committed 4 years ago

8159af67

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

leanprover-community-bot committed 4 years ago

468a9d56

Older