leanprover-community/mathlib

Pull Requests Commits

refactor(measure_theory): add typeclasses for measurability of operations (#6832)

urkud committed 4 years ago

0e4760b3

lint(*): split long lines (#6918)

urkud committed 4 years ago

dc34b216

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

leanprover-community-bot committed 4 years ago

e129117c

feat(test/integration): add examples of computing integrals by simp (#6859)

benjamindavidson committed 4 years ago

879cb474

chore(category_theory/monads): remove empty file (#6915)

b-mehta committed 4 years ago

06b21d0f

refactor(geometry/manifold/algebra/smooth_functions): make `smooth_map_group` division defeq to `pi.has_div` (#6912)

ocfnash committed 4 years ago

27c86764

chore(topology/metric_space): golf, generalize, rename (#6849)

urkud committed 4 years ago

d1044139

refactor(representation_theory/maschke): replaces `¬(ring_char k ∣ fintype.card G)` with `invertible (fintype.card G : k)` instance (#6901)

awainverse committed 4 years ago

cc7e722a

feat(data/nat/log): add some lemmas and monotonicity (#6899)

hallow-world committed 4 years ago

d32f9c72

feat(group_theory/order_of_element): order_of is the same in a submonoid (#6876)

tb65536 committed 4 years ago

5ecb1f73

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

leanprover-community-bot committed 4 years ago

5c95d480

feat(algebra/module): pull-back module structures along homomorphisms (#6895)

eric-wieser committed 4 years ago

3fe67c86

chore(algebra/smul_with_zero): add missing injective / surjective transferring functions (#6892)

eric-wieser committed 4 years ago

4b261a86

refactor(topology/continuous_functions): change file layout (#6890)

kim-em committed 4 years ago

832a2eb9

refactor(analysis/normed_space/basic): add semi_normed_group (#6888)

riccardobrasca committed 4 years ago

99c23eaf

feat(group_theory/perm/cycles): is_cycle_of_is_cycle_pow (#6871)

tb65536 committed 4 years ago

bc33f1a9

feat(algebra/big_operators/basic): add lemmas for a product with two non one factors (#6826)

paulvanwamelen committed 4 years ago

5eead090

feat(linear_algebra/bilinear_form): generalize some constructions to the noncomm case (#6824)

hrmacbeth committed 4 years ago

cfd1a4cb

feat(order/lattice): add complete_semilattice_Sup/Inf (#6797)

kim-em committed 4 years ago

ec26d96a

chore(category_theory/monoidal): golf some proofs (#6894)

b-mehta committed 4 years ago

e36656ee

chore(data/equiv/transfer_instance): reuse existing proofs (#6868)

eric-wieser committed 4 years ago

e21b4bcb

feat(ring_theory/int/basic): Induction, nat_abs and units (#6733)

thejohncrafter committed 4 years ago

9e00c2bc

feat(geometry/manifold/algebra/smooth_functions): simp lemmas for coercions to functions (#6893)

ocfnash committed 4 years ago

ca7dca39

chore(algebra/group): rename `is_unit_unit` to `units.is_unit` (#6886)

urkud committed 4 years ago

902b01d8

chore(data/pi,algebra/group/pi): reorganize proofs (#6869)

urkud committed 4 years ago

e43d9649

feat(*): add more lemmas about `set.piecewise` (#6862)

urkud committed 4 years ago

3566cbba

feat(dynamics/ergodic/conservative): define conservative systems, formalize Poincaré recurrence thm (#2311)

urkud committed 4 years ago

ef7fe6f9

feat(geometry/manifold/mfderiv): differentiability of `f : E ≃L[𝕜] E'` (#6850)

urkud committed 4 years ago

f0bfb25c

feat(linear_algebra/dual): add the dual map (#6807)

kex-y committed 4 years ago

2b71c803

feat(topology/bcf): better dist_lt_of_* lemmas (#6781)

kim-em committed 4 years ago

8addf9a7

Newer Older