leanprover-community/mathlib

Pull Requests Commits

Merge remote-tracking branch 'origin/master' into finsupp_bilin

hrmacbeth committed 4 years ago

9a614116

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

feat(ring_theory/polynomial/symmetric): degrees_esymm (#6718)

pechersky committed 4 years ago

6ae9f000

feat(group_theory/perm/sign): power has smaller support (#6872)

tb65536 committed 4 years ago

34a33172

feat(ring_theory/ideal/operations): add an instance (#6717)

riccardobrasca committed 4 years ago

adc5f9d6

chore(topology/sheaves): speed up a slow proof (#6879)

kim-em committed 4 years ago

fb495299

refactor(algebra/field): allow custom `div` (#6874)

urkud committed 4 years ago

c658f5cc

feat(group_theory/perm_basic): Lemma swap_apply_apply (#6870)

tb65536 committed 4 years ago

c07c3107

feat(measure_theory/interval_integral): weaken assumption in `integral_non_ae_measurable` (#6858)

benjamindavidson committed 4 years ago

0977b203

refactor(topology/algebra): define `has_continuous_smul`, use for topological semirings and algebras (#6823)

urkud committed 4 years ago

03f0bb1f

feat(category_theory/triangulated/rotate): add definition of rotation and inverse rotation of triangles and their morphisms (#6803)

l-kershaw committed 4 years ago

5c93c2d0

Older