leanprover-community/mathlib3

Pull Requests Commits

make suggested changes

winston-h-zhang committed 4 years ago

2817539a

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

leanprover-community-bot committed 4 years ago

013a84eb

chore(data/list): drop `list.is_nil` (#7269)

urkud committed 4 years ago

8bf9fd58

chore(algebra/*): add back nat_algebra_subsingleton and add_comm_monoid.nat_semimodule.subsingleton (#7263)

eric-wieser committed 4 years ago

3ad4dabf

winston-h-zhang committed 4 years ago

59d0f4f3

winston-h-zhang committed 4 years ago

48c77617

winston-h-zhang committed 4 years ago

eaad930f

winston-h-zhang committed 4 years ago

5c4a4000

intitial commit

winston-h-zhang committed 4 years ago

f1010c5a

chore(*): speed up slow proofs (#7253)

sgouezel committed 4 years ago

0dfac6eb

feat(algebra/module/submodule_lattice): add lemmas for nat submodules (#7221)

riccardobrasca committed 4 years ago

829d7733

feat(data/{int, nat}/parity): rename `ne_of_odd_sum` (#7261)

benjamindavidson committed 4 years ago

6f0c4fb3

chore(algebra/group): missed generalizations to mul_one_class (#7259)

eric-wieser committed 4 years ago

fc5e8cb0

fix(equiv/ring): fix bad typeclasses on ring_equiv.trans_apply (#7258)

eric-wieser committed 4 years ago

184e0fe4

feat(linear_algebra/eigenspace): `mem_maximal_generalized_eigenspace` (#7162)

ocfnash committed 4 years ago

77f5fb33

feat(algebra/module/projective): add projective module (#6813)

kbuzzard committed 4 years ago

15a64f53

feat(data/{int, nat, rat}/cast): extensionality lemmas (#6788)

thejohncrafter committed 4 years ago

272e2d22

feat(topology/algebra/ordered): IVT for the unordered interval (#7237)

benjamindavidson committed 4 years ago

43f63d99

feat(tactic/simps): use new options in library (#7095)

fpvandoorn committed 4 years ago

5993b90e

chore(data/set/basic): add `set.subsingleton.pairwise_on` (#7257)

urkud committed 4 years ago

dbc6574c

feat(data/nat/parity): update to match int/parity (#7156)

benjamindavidson committed 4 years ago

f6132e4d

feat(data/int/parity): update to match nat/parity (where applicable) (#7155)

benjamindavidson committed 4 years ago

969c6a3e

feat(group_theory/submonoid/operations): add lemmas (#7219)

riccardobrasca committed 4 years ago

30ee691e

feat(data/complex): numerical bounds on log 2 (#7146)

b-mehta committed 4 years ago

d107d825

feat(topology/continuous_function): on a subsingleton X, there is only one subalgebra R C(X,R) (#7247)

kim-em committed 4 years ago

7f541b4e

feat(data/finset/lattice): mem_sup, mem_sup' (#7245)

kim-em committed 4 years ago

cab0481e

feat(set_theory/surreal): add add_monoid instance (#7228)

apurvnakade committed 4 years ago

3953378b

feat(topology/algebra/mul_action.lean): add smul_const (#7242)

YaelDillies committed 4 years ago

a6f62a74

chore(data/set/finite): rename some lemmas (#7241)

urkud committed 4 years ago

4d4b501e

feat(algebra/lie/basic): define the `module` and `lie_module` structures on morphisms of Lie modules (#7225)

ocfnash committed 4 years ago

043d046a

Newer Older