leanprover-community/mathlib3

Pull Requests Commits

feat(group/theory/specific_groups/dihedral): add beginning of iff statement for center

Fontkodo committed 4 years ago

62cf5ef7

feat(group_theory/specific_groups/dihedral): add explicit definition of center

Fontkodo committed 4 years ago

55316987

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

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

leanprover-community-bot committed 4 years ago

d40e40c2

ci(.github/workflows/build.yml): check counterexamples (#7618)

bryangingechen committed 4 years ago

72e4cca4

feat(set_theory/game): add mul_one and mul_assoc for pgames (#7610)

apurvnakade committed 4 years ago

84a27d60

refactor(measure_theory/haar_measure): move general material to content.lean, make content a structure (#7615)

sgouezel committed 4 years ago

aedd12da

feat(algebra/ordered_group, algebra/ordered_ring): add some lemmas about abs (#7612)

Ruben-VandeVelde committed 4 years ago

1b098c06

feat(category_theory/category): initialize simps (#7605)

fpvandoorn committed 4 years ago

b98d8408

chore(order/fixed_point): add docstring for Knaster-Tarski theorem (#7589)

YaelDillies committed 4 years ago

9084a3c7

feat(analysis/normed_space): normed_group punit (#7616)

kim-em committed 4 years ago

c8a2fd7f

fix(tactic/lift): elaborate the type better (#7598)

fpvandoorn committed 4 years ago

2bd4bb69

feat(algebra/subalgebra): two equal subalgebras are equivalent (#7590)

Vierkantor committed 4 years ago

632783df

feat(analysis/calculus/local_extr): A polynomial's roots are bounded by its derivative (#7571)

benjamindavidson committed 4 years ago

4d909f41

fix(tactic/simps): fix bug (#7433)

fpvandoorn committed 4 years ago

ee6a9fa7

fix(tactic/simps): remove occurrence of mk_mapp (#7432)

fpvandoorn committed 4 years ago

f1bcb903

feat(algebraic_topology): cosimplicial objects (#7614)

kim-em committed 4 years ago

65e76465

Older