leanprover-community/mathlib

Pull Requests Commits

Make `mul_action_hom_class`es

Vierkantor committed 4 years ago

eabef937

Vierkantor committed 4 years ago

a5f56ded

Vierkantor committed 4 years ago

f89c6b0d

`coe_fn_coe_base` doesn't need to be removed from the simp set anymore

Vierkantor committed 4 years ago

c83b0f33

Remove the `@[simp]` attribute from `coe_fn_coe_base`

Vierkantor committed 4 years ago

5ba8491c

`foo_hom_class` instances for `ring_equiv`

Vierkantor committed 4 years ago

b579f67a

Rename `is_foo_hom` to `foo_hom_class`

Vierkantor committed 4 years ago

dd627452

Delete unnecessary `coe_to_fun`

Vierkantor committed 4 years ago

3ab512ea

WIP: some deduplication of the lemmas

Vierkantor committed 4 years ago

aae564ad

Generalize `map_inv`, `map_div` and their dependencies

Vierkantor committed 4 years ago

fd4ec00f

Vierkantor committed 4 years ago

e48bcee6

`is_{one,mul,monoid,monoid_with_zero}_hom`

Vierkantor committed 4 years ago

3660e66a

`is_{add,zero,add_monoid}_hom`

Vierkantor committed 4 years ago

f49270ed

doc(group_theory/sylow): module doc (#6477)

Julian-Kuelshammer committed 4 years ago

edbbecbe

feat(data/finsupp/basic): add support_nonempty_iff and nonzero_iff_exists (#6530)

adomani committed 4 years ago

d32bb6ed

feat(linear_algebra/clifford_algebra): add definitions of the conjugation operators and some API (#6491)

eric-wieser committed 4 years ago

ca96bfbe

feat(data/mv_polynomial/equiv): generalize ring_equiv_congr (#6420)

riccardobrasca committed 4 years ago

deb3d452

chore(topology/algebra/*): tendsto namespacing (#6528)

hrmacbeth committed 4 years ago

3329ec4e

refactor(big_operators/basic): move prod_mul_prod_compl (#6526)

kim-em committed 4 years ago

76aee25d

feat(topology/instances/real): generalize 'compact_space I' to 'compact_space (Icc a b)' (#6523)

kim-em committed 4 years ago

d7fa1bc8

chore(*/sub*): tidy up inherited algebraic structures from parent objects (#6509)

eric-wieser committed 4 years ago

2f357794

feat(category_theory/subobject): factoring morphisms through subobjects (#6302)

kim-em committed 4 years ago

f4db322f

feat(algebra/star): the Bell/CHSH/Tsirelson inequalities (#4687)

kim-em committed 4 years ago

8289518d

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

leanprover-community-bot committed 4 years ago

28378076

chore(algebra/ordered_group): put to_additive on lemmas about linear_ordered_comm_group (#6506)

eric-wieser committed 4 years ago

3c9399d1

feat(data/list/basic): add `list.prod_eq_zero(_iff)` (#6504)

urkud committed 4 years ago

d4ac4c3e

feat(data/equiv/fin): fin_add_flip and fin_rotate (#6454)

kim-em committed 4 years ago

a852bf40

chore(ring_theory/{subring,integral_closure}): simplify a proof, remove redundant instances (#6513)

eric-wieser committed 4 years ago

9c48eb18

feat(algebra/field): add function.injective.field (#6511)

eric-wieser committed 4 years ago

eec54d05

refactor(ring_theory/polynomial/chebyshev): move lemmas around (#6510)

hrmacbeth committed 4 years ago

3309ce27

Older