leanprover-community/mathlib3

Pull Requests Commits

chore(algebra/module/submodule): add missing coe lemmas (#7205)

eric-wieser committed 4 years ago

50a843e0

feat(linear_algebra/basic): add span_eq_add_submonoid.closure (#7200)

riccardobrasca committed 4 years ago

14c625e1

feat(number_theory/bernoulli): golf (#7197)

benjamindavidson committed 4 years ago

0f3ca672

chore(topology/vector_bundle): generalize to topological semimodules (#7183)

urkud committed 4 years ago

6a4d298c

feat(algebra/group_with_zero): non-associative monoid_with_zero (#7176)

eric-wieser committed 4 years ago

f92dc6c0

refactor(algebra/big_operators/order): use `to_additive` (#7173)

urkud committed 4 years ago

adfeb249

feat(data/nat/basic, data/nat/prime): add various lemmas (#7171)

Ruben-VandeVelde committed 4 years ago

5806a946

feat(category_theory/subobject): proof golf and some API (#7170)

TwoFX committed 4 years ago

4b835cc1

feat(analysis/special_functions/trigonometric): periodicity of sine, cosine (#7107)

benjamindavidson committed 4 years ago

dbd468d9

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

leanprover-community-bot committed 4 years ago

3a64d116

chore(data/fin,data/finset): a few lemmas (#7168)

urkud committed 4 years ago

c73b1653

feat(algebra/ordered_group): proof of le without density (#7191)

b-mehta committed 4 years ago

f74213bf

feat(field_theory/algebraic_closure): define `is_alg_closed.splits_codomain` (#7187)

Vierkantor committed 4 years ago

60060c3c

chore(algebra/group_power/basic): `pow_abs` does not need commutativity (#7178)

eric-wieser committed 4 years ago

3d67b696

chore(category_theory/subobject): split off specific subobjects (#7167)

TwoFX committed 4 years ago

e4843ea0

feat(topological/homeomorph): the image of a set (#7147)

kim-em committed 4 years ago

74e1e83e

feat(data/nat/basic): (∀ a : ℕ, m ∣ a ↔ n ∣ a) ↔ m = n (#7132)

adomani committed 4 years ago

5052ad95

feat(algebra/big_operators/finprod): add a few lemmas (#7130)

urkud committed 4 years ago

4605b55d

feat(topology/algebra,geometry/manifold): continuity and smoothness of locally finite products of functions (#7128)

urkud committed 4 years ago

49fd7195

feat(algebra/big_operators): some lemmas on big operators and `fin` (#7119)

Vierkantor committed 4 years ago

d820a9d7

feat(archive/imo): IMO 1977 Q6 (#7097)

peakpoint committed 4 years ago

8d3e8b5b

feat(order/filter/*, topology/subset_properties): Filter Coprod (#7073)

AlexKontorovich committed 4 years ago

456e5af8

feat(group_theory/perm/cycle_type): Cycle type of a permutation (#6999)

awainverse committed 4 years ago

89196b20

feat(order/ideal, order/pfilter, order/prime_ideal): added `ideal_inter_nonempty`, proved that a maximal ideal is prime (#6924)

atarnoam committed 4 years ago

5775ef75

feat(topology/sheaves): Induced map on stalks (#7092)

justus-springer committed 4 years ago

3df0f773

feat(ring_theory/hahn_series): a `finsupp` of Hahn series is a `summable_family` (#7091)

awainverse committed 4 years ago

98c483b9

chore(algebra/direct_sum_graded): golf proofs (#7029)

gnprice committed 4 years ago

f444128f

feat(archive/100-theorems-list): add proof of Heron's formula (#6989)

matt-kempster committed 4 years ago

3379f3ed

feat(geometry/manifold/instances/units_of_normed_algebra): the units of a normed algebra are a topological group and a smooth manifold (#6981)

Nicknamen committed 4 years ago

27157699

feat(algebra/direct_sum_graded): `A 0` is a ring, `A i` is an `A 0`-module, and `direct_sum.of A 0` is a ring_hom (#6851)

eric-wieser committed 4 years ago

e4edf46d

Newer Older