leanprover-community/mathlib

Pull Requests Commits

benjamindavidson committed 4 years ago

60ed8828

benjamindavidson committed 4 years ago

ac064c00

benjamindavidson committed 4 years ago

a36c1587

benjamindavidson committed 4 years ago

3b496d54

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

eric-wieser committed 4 years ago

3ad4dabf

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

feat(data/real): Inf is nonneg (#7223)

b-mehta committed 4 years ago

aa44de5b

feat(linear_algebra): maximal linear independent (#7160)

PatrickMassot committed 4 years ago

c68e718a

chore(.github/workflows/build.yml): update elan script URL (#7234)

bryangingechen committed 4 years ago

ce667c41

refactor(topology/algebra/module): `map_smul` argument swap (#7233)

YaelDillies committed 4 years ago

20db2fb2

Older