leanprover-community/mathlib

Pull Requests Commits

awainverse committed 3 years ago

b6f0715f

awainverse committed 3 years ago

2fcfa1cd

Merge remote-tracking branch 'origin/partitioned_formula' into definable_with_parameters

awainverse committed 3 years ago

3f7b157b

awainverse committed 3 years ago

78334db1

awainverse committed 3 years ago

4faad3cb

awainverse committed 3 years ago

a79f58d6

awainverse committed 3 years ago

6e12a3d7

awainverse committed 3 years ago

66267ced

awainverse committed 3 years ago

d1b83244

awainverse committed 3 years ago

8a4302df

awainverse committed 3 years ago

28ff625e

awainverse committed 3 years ago

80d03fc3

chore(data/finsupp/pointwise): golf using injective lemmas (#12086)

eric-wieser committed 3 years ago

b395a671

chore(topology/continuous_function/bounded): golf algebra instances (#12082)

eric-wieser committed 3 years ago

0ab9b5f3

chore(ring_theory/fractional_ideal): golf (#12076)

eric-wieser committed 3 years ago

d86ce027

feat(logic/basic): Better congruence lemmas for `or`, `or_or_or_comm` (#12004)

YaelDillies committed 3 years ago

15c6eee7

feat(category_theory/category/PartialFun): The category of types with partial functions (#11866)

YaelDillies committed 3 years ago

5e3d465c

awainverse committed 3 years ago

cafac86b

awainverse committed 3 years ago

3e508ae7

awainverse committed 3 years ago

3bd2e47a

awainverse committed 3 years ago

1acb8cb1

awainverse committed 3 years ago

4bafeb15

awainverse committed 3 years ago

48f65185

docs(group_theory/semidirect_product): fix typo in module docs (#12083)

nomeata committed 3 years ago

3c78d00a

feat(algebra/char_p/basic): Generalize `frobenius_inj`. (#12079)

adamtopaz committed 3 years ago

3107a831

feat(data/finset/basic): When `insert` is injective and other lemmas (#11982)

YaelDillies committed 3 years ago

0eb160a5

feat(order/antisymmetrization): Turning a preorder into a partial order (#11728)

YaelDillies committed 3 years ago

6bcb12c1

chore(topology/algebra/mul_action): rename type variables (#12020)

urkud committed 3 years ago

8a286af6

awainverse committed 3 years ago

a6c737b8

awainverse committed 3 years ago

0a9f5219

Older