leanprover-community/mathlib

Pull Requests Commits

adamtopaz committed 4 years ago

b288b942

feat(data/polynomial/coeff): generalize polynomial.coeff_smul to match mv_polynomial.coeff_smul (#7663)

eric-wieser committed 4 years ago

ed4161c5

feat(data/int/parity, data/nat/parity): add some lemmas (#7624)

Ruben-VandeVelde committed 4 years ago

599712ff

refactor(topology/basic): use dot notation in `is_open.union` and friends (#7647)

sgouezel committed 4 years ago

697c8dd9

feat(data/polynomial/degree/definitions): `polynomial.degree_C_mul_X_le` (#7659)

benjamindavidson committed 4 years ago

c7a51977

fix(analysis/normed_space/normed_group_quotient): put lemmas inside namespace (#7653)

benjamindavidson committed 4 years ago

040ebea0

docs(field_theory/polynomial_galois_group): improve existing docs (#7586)

ericrbg committed 4 years ago

c1e9f942

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

leanprover-community-bot committed 4 years ago

1d4990e2

chore(algebra/homology): further dualization (#7657)

kim-em committed 4 years ago

918dcc0a

feat(algebraic_topology/simplicial_object): Some API for converting between simplicial and cosimplicial (#7656)

adamtopaz committed 4 years ago

aee918b8

feat(algebraic_topology/simplicial_object): Whiskering of simplicial objects. (#7651)

adamtopaz committed 4 years ago

24d2713d

feat(linear_algebra/basis) remove several [nontrivial R] (#7642)

riccardobrasca committed 4 years ago

0bcfff99

feat(algebra/homology/homological_complex): Dualizes some constructions (#7643)

adamtopaz committed 4 years ago

a51d1e0e

chore(data/set/basic): add `set.compl_eq_compl` (#7641)

ericrbg committed 4 years ago

e2756041

refactor(linear_algebra/dimension): generalize definition of `module.rank` (#7634)

kim-em committed 4 years ago

c2114d45

feat(algebra/opposites): add `has_scalar (opposite α) α` instances (#7630)

eric-wieser committed 4 years ago

e6c787fe

feat(analysis/normed_space): the category of seminormed groups (#7617)

kim-em committed 4 years ago

1a2781a7

feat(logic/is_empty): Add is_empty typeclass (#7606)

fpvandoorn committed 4 years ago

3694945d

feat(analysis/normed_group): quotients (#7603)

PatrickMassot committed 4 years ago

1b864c0d

feat(linear_algebra/matrix): slightly generalize `smul_left_mul_matrix` (#7632)

Vierkantor committed 4 years ago

f900513a

feat(data/polynomial): the `d-1`th coefficient of `polynomial.map` (#7639)

Vierkantor committed 4 years ago

b8a69951

feat(ring_theory/power_basis): the dimension of a power basis is positive (#7638)

Vierkantor committed 4 years ago

ccf5188f

feat(data/multiset): the product of inverses is the inverse of the product (#7637)

Vierkantor committed 4 years ago

4ab0e350

feat(linear_algebra): a finite free module has a unique findim (#7631)

Vierkantor committed 4 years ago

818dffa0

feat(linear_algebra/basic): add_monoid_hom_lequiv_int (#7629)

kim-em committed 4 years ago

36e01274

refactor(algebra/homology/homotopy): avoid needing has_zero_object (#7621)

kim-em committed 4 years ago

d201a182

refactor(data/finsupp/antidiagonal): Make antidiagonal a finset (#7595)

BoltonBailey committed 4 years ago

07fb3d7e

feat(data/finset/basic): perm_of_nodup_nodup_to_finset_eq (#7588)

pechersky committed 4 years ago

8394e594

feat(algebra/lie/weights): the zero root subalgebra is self-normalizing (#7622)

ocfnash committed 4 years ago

739d93c6

doc(counterexamples/canonically_ordered_comm_semiring_two_mul): fix url (#7625)

gebner committed 4 years ago

2077c90c

Older