leanprover-community/mathlib

Pull Requests Commits

feat(linear_algebra/tensor_product): add id_apply and comp_apply for ltensor and rtensor (#15628)

kbuzzard committed 3 years ago

a1fdc999

refactor(data/{finite,fintype}): move some lemmas to `data.fintype.basic` (#15626)

urkud committed 3 years ago

aed4c494

chore(*): Rename `normed_group` to `normed_add_comm_group` (#15619)

YaelDillies committed 3 years ago

d1bd9c5d

feat(set_theory/zfc/basic): `∈` is well-founded on classes (#15544)

vihdzp committed 3 years ago

989fe520

feat(data/list/of_fn): lemmas to turn quantifiers over lists to quantifiers over tuples (#15433)

eric-wieser committed 3 years ago

639fe5ab

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

leanprover-community-bot committed 3 years ago

b3bcb796

feat(analysis/normed_space/linear_isometry): add defs and lemmas (#15650)

urkud committed 3 years ago

4a4c2753

feat(analysis/inner_product_space/positive): definition and basic facts about positive operators (#15470)

ADedecker committed 3 years ago

0179605f

feat(number_theory/legendre_symbol/add_character): add file introducing additive characters (#15499)

MichaelStollBayreuth committed 3 years ago

983c737a

fix(*): fix typos I made yesterday (#15627)

urkud committed 3 years ago

c9ba943d

refactor(*): rename `nondiscrete_normed_field` (#15625)

j-loreaux committed 3 years ago

ef901ea6

refactor(data/set/countable): golf using `_root_.countable`, review API (#15624)

urkud committed 3 years ago

4050b906

chore(algebra/lie/direct_sum): remove `direct_sum.lie_algebra_is_internal` (#15631)

eric-wieser committed 3 years ago

c0cc689b

feat(data/finset/basic): There is exactly one set in empty types (#15607)

YaelDillies committed 3 years ago

92e96605

feat(order/partition/finpartition): Bound size of a bit of `finpartition.atomise` (#15350)

YaelDillies committed 3 years ago

6537ae9c

feat(combinatorics/simple_graph/density): Bound on the difference between edge densities (#15353)

YaelDillies committed 3 years ago

7c94fe71

feat(ring_theory/noetherian): Finitely generated idempotent ideal is principal. (#15561)

erdOne committed 3 years ago

106f0ac9

feat(set_theory/game/nim): make the file `noncomputable theory` (#15367)

vihdzp committed 3 years ago

282da0c1

feat(order/upper_lower): Upper closure of a set (#15581)

YaelDillies committed 3 years ago

ab6bcd63

feat(data/polynomial/degree/definitions): redefine `polynomial.degree` as `p.support.max` (#15199)

adomani committed 3 years ago

1e024cb6

feat(analysis/locally_convex/with_seminorms): in a normed space, von Neumann bounded = metric bounded (#15124)

ADedecker committed 3 years ago

db22f697

move(order/{boolean_algebra → basic}): move `has_compl` and trivial instances (#15602)

vihdzp committed 3 years ago

b2ba27ce

feat(topology/metric_space/isometry): use namespace, add lemmas (#15591)

urkud committed 3 years ago

0b1e039b

fix(data/json): `rbmap string α` never serializes to `null` (#15622)

eric-wieser committed 3 years ago

b93a64da

feat(order/boolean_algebra): A bounded generalized boolean algebra is a boolean algebra (#15606)

YaelDillies committed 3 years ago

81e26435

feat(data/set/function): add lemmas about `set.restrict` (#15605)

urkud committed 3 years ago

6b93ea7e

feat(topology/order): upgrade some lemmas to `iff`s (#15617)

urkud committed 3 years ago

8ad82e4b

chore(analysis/normed/field/unit_ball): cleanup instances (#15615)

urkud committed 3 years ago

db107767

feat(topology/maps): add 2 lemmas, `open function` (#15612)

urkud committed 3 years ago

51891bef

feat(logic/equiv/local_equiv): add 2 lemmas (#15611)

urkud committed 3 years ago

1a73c7ee

Newer Older