leanprover-community/mathlib

Pull Requests Commits

Update ring.lean

vihdzp committed 3 years ago

ee57a418

Update monoid.lean

vihdzp committed 3 years ago

4802cf5a

feat(order/filter/ultrafilter): `pure`, `map`, and `comap` lemmas (#15187)

YaelDillies committed 3 years ago

37c27774

feat(linear_algebra/unitary_group): better constructor (#15209)

hrmacbeth committed 3 years ago

861589f2

chore(set_theory/ordinal/arithmetic): review cast API (#14757)

vihdzp committed 3 years ago

983fdd6b

feat(set_theory/ordinal/basic): order type of naturals is `ω` (#15178)

vihdzp committed 3 years ago

6d245b26

feat(combinatorics/simple_graph/subgraph): add `subgraph.comap` and subgraph of subgraph coercion (#14877)

kmill committed 3 years ago

7cf0ae6a

Removed unnecessary assumption in `map_injective_of_injective` (#15184)

nick-kuhn committed 3 years ago

d3d35395

feat(logic/equiv/set): define `equiv.set.pi` (#15176)

urkud committed 3 years ago

f26a0a35

feat(analysis/locally_convex/basic): a few lemmas about balanced sets (#14876)

mcdoll committed 3 years ago

c5b6fe54

feat(set_theory/ordinal/arithmetic): tweak `type_add` and `type_mul` (#15193)

vihdzp committed 3 years ago

fefd449d

feat(analysis/normed_space/star/basic): make starₗᵢ apply to normed star groups (#15173)

j-loreaux committed 3 years ago

f39bd5f0

feat(combinatorics/simple_graph/hasse): The Hasse diagram of `α × β` (#14978)

YaelDillies committed 3 years ago

8a38a697

feat(combinatorics/additive/ruzsa_covering): The Ruzsa covering lemma (#14697)

YaelDillies committed 3 years ago

1a54e4da

chore(data/zmod/defs): shuffle files around (#15142)

ericrbg committed 3 years ago

2d5b45c8

feat(data/rat/defs): add denominator as pnat (#15101)

Jon Eugster committed 3 years ago

11cdccb8

chore(data/nat/squarefree): fix a tactic doc typo for norm num extension (#15189)

alexjbest committed 3 years ago

feb34df6

fix(data/fintype/basic): move card_subtype_mono into the fintype namespace (#15185)

linesthatinterlace committed 3 years ago

5a5d2909

feat(analysis/normed_space/lp_space): normed_algebra structure (#15086)

eric-wieser committed 3 years ago

1937dff0

doc(tactic/wlog): use markdown lists rather than indentation (#15113)

eric-wieser committed 3 years ago

e74e5349

feat(topology/metric_space/hausdorff_distance): Thickening a compact inside an open (#14926)

YaelDillies committed 3 years ago

0bc51f02

feat(combinatorics/simple_graph/prod): Box product (#14867)

YaelDillies committed 3 years ago

93be74b1

feat(data/finset/basic): Coercion of a product of finsets (#15011)

YaelDillies committed 3 years ago

7c070c4d

feat(data/set/basic,order/filter/basic): add semiconj lemmas about images and maps (#14970)

eric-wieser committed 3 years ago

d34b3306

chore(topology/algebra/semigroup): golf file (#14957)

vihdzp committed 3 years ago

563a51af

feat(topology/algebra/uniform_group): `uniform_group` is preserved by Inf and comap (#14889)

ADedecker committed 3 years ago

ba9f346a

refactor(set_theory/cardinal/basic): migrate from `fintype` to `finite` (#15175)

urkud committed 3 years ago

6eeb941c

feat(set_theory/ordinal/arithmetic): tweak theorems about `0` and `1` (#15174)

vihdzp committed 3 years ago

a3c647bb

feat(topology/algebra/infinite_sum): Double sum is equal to a single value (#15157)

dtumad committed 3 years ago

f0f40704

chore(tactic/lift): move a proof to `subtype.exists_pi_extension` (#15098)

urkud committed 3 years ago

8927a02c

Older