leanprover-community/mathlib3

Pull Requests Commits

Finish `card_le_card_of_linear_independent`

Vierkantor committed 4 years ago

52843942

Vierkantor committed 4 years ago

44ae231c

Vierkantor committed 4 years ago

9948b78a

Vierkantor committed 4 years ago

fd88e705

Vierkantor committed 4 years ago

83929146

Vierkantor committed 4 years ago

c6f83d89

Vierkantor committed 4 years ago

9395a347

Vierkantor committed 4 years ago

fa2277ee

Vierkantor committed 4 years ago

87361c2c

chore(algebra/*): move some lemmas to `div_inv_monoid` (#5552)

urkud committed 4 years ago

409ea425

chore(data/fintype/card): generalize `equiv.prod_comp` to `function.bijective.prod_comp` (#5551)

urkud committed 4 years ago

06a11fd5

feat(analysis/normed_space/inner_product): upgrade orthogonal projection to a continuous linear map (#5543)

hrmacbeth committed 4 years ago

ea3815fb

feat(algebra/big_operators/nat_antidiagonal): add prod_antidiagonal_eq_prod_range_succ (#5528)

kbuzzard committed 4 years ago

b57d562c

feat(data/fin): there is at most one `order_iso` from `fin n` to `α` (#5499)

urkud committed 4 years ago

c32efeae

chore(*): golf some proofs (#5548)

urkud committed 4 years ago

8aa23326

chore(data/real/cau_seq): golf some proofs (#5545)

urkud committed 4 years ago

e0030ffe

chore(linear_algebra/basic): notation for span of a singleton (#5538)

hrmacbeth committed 4 years ago

b542cfbc

doc(lint/type_classes): add has_coe_to_fun linter (#5546)

fpvandoorn committed 4 years ago

fcbaf625

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

leanprover-community-bot committed 4 years ago

d2bde119

feat(logic/basic): exists_unique_false simp lemma (#5544)

pechersky committed 4 years ago

54bf708d

refactor(analysis/analytic/basic): redefine `formal_multilinear_series.radius` (#5349)

urkud committed 4 years ago

0830bfd4

chore(analysis/normed_space/inner_product): notation for orthogonal complement (#5536)

hrmacbeth committed 4 years ago

10f6c151

feat(field_theory/galois): is_galois.tfae (#5542)

tb65536 committed 4 years ago

cca63650

chore(algebra): move lemmas from ring_theory.algebra_tower to algebra.algebra.tower (#5506)

kckennylau committed 4 years ago

b04aeb5e

feat(data/tprod): finite products of types (#5385)

fpvandoorn committed 4 years ago

a40f31fb

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

leanprover-community-bot committed 4 years ago

611b73eb

feat(field_theory/algebraic_closure): algebraically closed fields have no nontrivial algebraic extensions (#5537)

dtumad committed 4 years ago

9c46cadc

chore(algebra/field): use `K` as a type variable (#5535)

urkud committed 4 years ago

6e0d0fa4

feat(measure_theory): various additions (#5389)

fpvandoorn committed 4 years ago

99881936

feat(order/lattice_intervals): lattice structures on intervals in lattices (#5496)

awainverse committed 4 years ago

f1d2bc60

Older