leanprover-community/mathlib

Pull Requests Commits

refactor(group_theory/commutator): Use commutator notation in `commutator_normal` (#12575)

tb65536 committed 4 years ago

6c04fcf4

feat(algebra/group/to_additive + a few more files): make `to_additive` convert `unit` to `add_unit` (#12564)

adomani committed 4 years ago

84cbbc98

feat(data/zmod/basic): some lemmas about coercions (#12571)

eric-wieser committed 4 years ago

869ef84f

chore(*): clear up some excessive by statements (#12570)

alexjbest committed 4 years ago

6fdb1d5d

feat(field_theory/is_alg_closed/basic): add `is_alg_closed.infinite` (#12566)

Jlh18 committed 4 years ago

45c22c0d

feat(tactic/norm_num_command): add user command to run norm_num on an expression (#12550)

kmill committed 4 years ago

0e93816c

chore(*): remove lines claiming to introduce variables (#12569)

adomani committed 4 years ago

f654a86a

chore(order/galois_connection): Make lifting instances reducible (#12559)

YaelDillies committed 4 years ago

4a59a4d4

chore(cardinal_divisibility): tiny golf (#12567)

ericrbg committed 4 years ago

788ccf07

feat(data/equiv/mul_add): add to_additive attribute to `group.is_unit` (#12563)

adomani committed 4 years ago

cd111e94

chore(set_theory/ordinal_arithmetic): Make auxiliary result private (#12562)

vihdzp committed 4 years ago

41f5c176

chore(measure_theory/function/convergence_in_measure): golf proof with Borel-Cantelli (#12551)

kex-y committed 4 years ago

4048a9be

feat(set_theory/ordinal_arithmetic): `add_eq_zero_iff`, `mul_eq_zero_iff` (#12561)

vihdzp committed 4 years ago

d56a9bc2

refactor(group_theory/commutator): Generalize `map_commutator_element` (#12555)

tb65536 committed 4 years ago

1e560a67

refactor(topology/opens): Turn `opens.gi` into a Galois coinsertion (#12547)

YaelDillies committed 4 years ago

24e3b5f5

feat(group_theory/double_cosets): definition of double cosets and some basic lemmas. (#9490)

CBirkbeck committed 4 years ago

0fd99294

chore(linear_algebra/affine_space/affine_map): golf using the injective APIs (#12543)

eric-wieser committed 4 years ago

750ca956

fix(linear_algebra/quadratic_form/basic): align diamonds in the nat- and int- action (#12541)

eric-wieser committed 4 years ago

8836a42d

feat(field_theory/krull_topology): added krull_topology_totally_disconnected (#12398)

Sebastian-Monnet committed 4 years ago

9e288527

feat(topology/opens): The frame of opens of a topological space (#12546)

YaelDillies committed 4 years ago

bab039fb

feat(category_theory/abelian/exact): `exact g.op f.op` (#12456)

jjaassoonn committed 4 years ago

9c2f6ebe

refactor(group_theory/commutator): Rename `commutator_containment` to `commutator_mem_commutator` (#12553)

tb65536 committed 4 years ago

ef25c4ca

doc(combinatorics/simple_graph/basic): fix typo (#12544)

kbuzzard committed 4 years ago

9facd190

chore(analysis/complex/upper_half_plane): use `coe` instead of `coe_fn` (#12532)

eric-wieser committed 4 years ago

0d6fb8a7

chore(data/polynomial): use dot notation for monic lemmas (#12530)

alexjbest committed 4 years ago

c4a34136

chore(set_theory/cardinal): `min` → `Inf` (#12517)

vihdzp committed 4 years ago

55d1f3e8

chore(linear_algebra/alternating): golf using injective APIs (#12536)

eric-wieser committed 4 years ago

5d405e2a

chore(algebra/module/linear_map): golf using injective APIs (#12535)

eric-wieser committed 4 years ago

bc9dda83

chore(data/{finsupp,dfinsupp}/basic): use the injective APIs (#12534)

eric-wieser committed 4 years ago

94e9bb55

chore(real/cau_seq_completion): put class in Prop (#12533)

PatrickMassot committed 4 years ago

b8d176e0

Newer Older