leanprover-community/mathlib

Pull Requests Commits

refactor(algebra/module/basic): relax the requirements on restrict_scalars

eric-wieser committed 4 years ago

3b9b21c1

chore(category_theory/limits/creates): fix typo in docstring (#6738)

b-mehta committed 4 years ago

9507a34f

chore(combinatorics/simple_graph): remove bad simp attribute (#6736)

b-mehta committed 4 years ago

6e1143ab

refactor(data/multiset/basic): consistently use 'nsmul' in names (#6735)

Ruben-VandeVelde committed 4 years ago

ce8a6ca0

feat(algebra/module/submodule): add `smul_of_tower_mem` (#6712)

eric-wieser committed 4 years ago

7e82bba0

feat(bounded_continuous_function): transport structure to C(α, β) when α compact (#6701)

kim-em committed 4 years ago

4ae81c2f

chore(analysis/normed_space/extend): provide a version without restrict_scalars (#6693)

eric-wieser committed 4 years ago

0b0fd528

refactor(linear_algebra/determinant): refactor proof of upper_two_block_triangular_det (#6690)

paulvanwamelen committed 4 years ago

6db70c98

feat(measure_theory/l2_space): L2 is an inner product space (#6596)

RemyDegenne committed 4 years ago

41191815

feat(number_theory/bernoulli): Faulhaber's theorem (#6409)

mo271 committed 4 years ago

fb28eac0

chore(group_theory/subgroup): fix typo in docstring (#6722)

jcommelin committed 4 years ago

83a4b8b9

feat(data/zsqrtd/basic): add some lemmas about conj, norm (#6715)

Ruben-VandeVelde committed 4 years ago

73922b54

feat(data/set/intervals/image_preimage, algebra/ordered_monoid): new typeclass for interval bijection lemmas (#6629)

apnelson1 committed 4 years ago

1f50530a

feat(ring_theory/algebraic data/real/irrational): add a proof that a transcendental real number is irrational (#6721)

adomani committed 4 years ago

13453191

chore(linear_algebra/determinant): redefine det using multilinear_map.alternatization (#6708)

eric-wieser committed 4 years ago

4b1d5886

feat(ring_theory/polynomial): Pochhammer polynomials (#6598)

kim-em committed 4 years ago

84933f12

feat(field_theory/normal): Tower of solvable extensions is solvable (#6643)

tb65536 committed 4 years ago

861f5946

refactor(group_theory/order_of_element): now makes sense for infinite monoids (#6587)

Julian-Kuelshammer committed 4 years ago

6f6b548b

feat(tactic/norm_num): support for nat.cast + int constructors (#6235)

digama0 committed 4 years ago

3e7a56ee

refactor(topology/metric_space/basic): add pseudo_metric (#6716)

riccardobrasca committed 4 years ago

d292fd7e

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

leanprover-community-bot committed 4 years ago

3936f5fd

feat(algebraic_topology/simplicial_objects + ...): Truncated simplicial objects + skeleton (#6711)

adamtopaz committed 4 years ago

b9ccb8fa

feat(topology/continuous_map): lattice structures (#6706)

kim-em committed 4 years ago

87c12abd

chore(linear_algebra/finite_dimensional): change instance (#6713)

urkud committed 4 years ago

40a0ac77

feat(topology/separation): `(closure s).subsingleton ↔ s.subsingleton` (#6707)

urkud committed 4 years ago

177020e4

feat(measure_theory/measure_space): define `quasi_measure_preserving` (#6699)

urkud committed 4 years ago

890066ac

chore(*): update to Lean 3.28.0c (#6691)

bryangingechen committed 4 years ago

f5f42bc9

feat(geometry/manifold/mfderiv): more lemmas (#6679)

urkud committed 4 years ago

a116025e

feat(topology/algebra): more on closure (#6675)

kim-em committed 4 years ago

214b8e84

chore(ring_theory/noetherian): add `fg_span` and `fg_span_singleton` (#6709)

urkud committed 4 years ago

8d8c3560

Older