leanprover-community/mathlib

Pull Requests Commits

feat(ring_theory/dedekind_domain/ideal): drop an unneeded assumption (#14444)

urkud committed 3 years ago

65031caf

fix(topology/algebra/group_completion): add lemmas about nsmul and zsmul and fix diamonds (#14846)

eric-wieser committed 3 years ago

273986ad

feat(data{finset,set}/pointwise): Pointwise monoids are domains (#14687)

YaelDillies committed 3 years ago

2a7bde04

refactor(algebra/{hom/equiv, ring/equiv}): rename `equiv_of_unique_of_unique` to `equiv_of_unique` (#14861)

vihdzp committed 3 years ago

481f9910

chore(set_theory/game/*): create `pgame` and `natural_ops` locales (#14856)

vihdzp committed 3 years ago

e1d7cc70

fix(tactic/norm_num): fix bad proof / bad test (#14852)

digama0 committed 3 years ago

67e026c8

chore(data/finsupp/fin): fix spacing (#14860)

vihdzp committed 3 years ago

8ac19d32

chore(set_theory/ordinal/natural_ops): use derive (#14859)

vihdzp committed 3 years ago

326465de

feat(data/fintype/basic): equivalence between `finset α` and `set α` for `fintype α` (#14840)

vihdzp committed 3 years ago

3b5441cb

feat(polynomial/ring_division): strengthen/generalize various lemmas (#14839)

alreadydone committed 3 years ago

87f47580

refactor(data/sym/basic): change notation for sym.cons (#14853)

kmill committed 3 years ago

125055b0

chore(data/nat/totient): golf a proof (#14851)

urkud committed 3 years ago

9df2762e

feat(order/monotone): Monotonicity of `prod.map` (#14843)

YaelDillies committed 3 years ago

f855a4ba

feat(logic/unique): functions from a `unique` type is `const` (#14823)

alreadydone committed 3 years ago

66d3f897

docs(linear_algebra): refer to `pi.basis_fun` in `pi.basis` (#14505)

Vierkantor committed 3 years ago

0b806ba6

feat(data/prod/basic): Involutivity of `prod.map` (#14845)

YaelDillies committed 3 years ago

c781c0ea

refactor(linear_algebra/exterior_algebra): redefine `exterior_algebra` as `clifford_algebra 0` (#14819)

eric-wieser committed 3 years ago

c1abe061

feat(data/dfinsupp/basic): add missing lemmas about `single` (#14815)

eric-wieser committed 3 years ago

320ea398

feat(algebra/order/pointwise): Supremum of pointwise operations (#13669)

YaelDillies committed 3 years ago

c5e13baa

feat(group_theory/group_action/sigma): Scalar action on a sigma type (#14825)

YaelDillies committed 3 years ago

f9c339ec

chore(algebra/group/basic): lemmas about `bit0`, `bit1`, and addition (#14798)

eric-wieser committed 3 years ago

ff40b2c1

feat(order/filter/bases): basis for directed (b)infi of filters (#14775)

ADedecker committed 3 years ago

df50b88a

feat(number_theory/number_field): add definitions and results about embeddings (#14749)

xroblot committed 3 years ago

2604c048

refactor(analysis/complex/upper_half_plane): move topology to a new file (#14748)

urkud committed 3 years ago

8263a4bf

feat(geometry/manifold/diffeomorph): some additions needed for smooth vector bundles (#14738)

fpvandoorn committed 3 years ago

804afcb0

feat(analysis/convex/join): Join of sets (#14676)

YaelDillies committed 3 years ago

04f45054

refactor(order/conditionally_complete_lattice): tweak `well_founded.conditionally_complete_linear_order_with_bot` (#14706)

vihdzp committed 3 years ago

29036740

refactor(number_theory/cyclotomic/*): refactor the definition of is_cyclotomic_extension (#14463)

riccardobrasca committed 3 years ago

ae5b6952

feat(analysis/normed/group/basic): `isometry.norm_map_of_map_zero` (#14836)

jsm28 committed 3 years ago

10a52752

feat(analysis/complex/upper_half_plane): add `upper_half_plane.mk` (#14795)

urkud committed 3 years ago

cf118ee6

Newer Older