leanprover-community/mathlib

Pull Requests Commits

chore(topology/algebra/uniform_mul_action): add `has_uniform_continuous_const_smul.op` (#12434)

eric-wieser committed 4 years ago

0a3d1440

chore(analysis/complex/basic): golf `norm_rat/int/int_of_nonneg` (#12433)

adomani committed 4 years ago

cac9242e

feat(set_theory/ordinal_arithmetic): `bsup` / `blsub` of function composition (#12381)

vihdzp committed 4 years ago

173f161b

mariainesdff committed 4 years ago

941369c3

suggested changes

mariainesdff committed 4 years ago

5b2d0458

chore(algebra/algebra/operations): add missing `@[elab_as_eliminator]` on recursors (#12440)

eric-wieser committed 4 years ago

a7217000

feat(set_theory/ordinal_arithmetic): `is_normal.blsub_eq` (#12379)

vihdzp committed 4 years ago

4a416bc2

feat(number_theory/cyclotomic/primitive_roots): generalize norm_eq_one (#12359)

riccardobrasca committed 4 years ago

b1444600

feat(linear_algebra/basic): some basic lemmas about dfinsupp.sum (#12214)

pbazin committed 4 years ago

53dc7ca3

refactor(algebra/category/Group/basic): Avoid data shuffle in `mul_equiv.to_Group_iso` (#12407)

YaelDillies committed 4 years ago

052d027f

feat(order/bounded): The universal set is unbounded (#12390)

vihdzp committed 4 years ago

0666dd5c

feat(counterexamples/seminorm_lattice_not_distrib): The lattice of seminorms is not distributive. (#12099)

pbazin committed 4 years ago

09c66fa1

feat(algebra/category): Module R is monoidal closed for comm_ring R (#12387)

kim-em committed 4 years ago

82a142d1

feat(data/nat/gcd): add coprime_prod_left and coprime_prod_right (#12268)

nomeata committed 4 years ago

e96cf5e6

feat(algebra/star/self_adjoint): define normal elements of a star monoid (#11991)

dupuisf committed 4 years ago

40524f19

refactor(linear_algebra/bilinear_form): split off matrix part (#12435)

mcdoll committed 4 years ago

544f45bc

feat(group_theory/torsion): all torsion monoids are groups (#12432)

Julian committed 4 years ago

5371338f

feat(polynomial/cyclotomic): some divisibility results (#12426)

ericrbg committed 4 years ago

1af53ff5

feat(data/{nat,int,rat}/cast, algebra/star/basic): lemmas about `star` on casts (#12418)

eric-wieser committed 4 years ago

54c286db

feat(ring_theory/ideal): more lemmas on ideals multiplied with submodules (#12401)

Vierkantor committed 4 years ago

9deac65c

feat(linear_algebra/clifford_algebra): lemmas about mapping submodules (#12399)

eric-wieser committed 4 years ago

2fc2d1b6

chore(linear_algebra/general_linear_group): replace coe_fn with coe in lemma statements (#12397)

eric-wieser committed 4 years ago

e84c1a96

feat(field_theory/cardinality): cardinality of fields & localizations (#12285)

ericrbg committed 4 years ago

4503732a

feat(group_theory/free_product): the 🏓-lemma (#12210)

nomeata committed 4 years ago

2c0fa829

feat(set_theory/cardinal_divisibility): add lemmas about divisibility in the cardinals (#12197)

ericrbg committed 4 years ago

f549c103

feat(ring_theory/witt_vector): classify 1d isocrystals (#12041)

robertylewis committed 4 years ago

2a05bb3a

chore(algebra/*): provide `non_assoc_ring` instances (#12414)

eric-wieser committed 4 years ago

066ffdb3

feat(data/int/basic): add three lemmas about ints, nats and int_nat_abs (#12380)

adomani committed 4 years ago

5d0960b6

fix(data/set/function): do not use reducible (#12377)

gebner committed 4 years ago

cdb69d5c

feat(algebra/ring/basic): generalize lemmas about differences of squares to non-commutative rings (#12366)

eric-wieser committed 4 years ago

363b7cd9

Newer Older