leanprover-community/mathlib3

Pull Requests Commits

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

Jlh18 committed 3 years ago

45c22c0d

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

kmill committed 3 years ago

0e93816c

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

adomani committed 3 years ago

f654a86a

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

YaelDillies committed 3 years ago

4a59a4d4

chore(cardinal_divisibility): tiny golf (#12567)

ericrbg committed 3 years ago

788ccf07

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

adomani committed 3 years ago

cd111e94

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

vihdzp committed 3 years ago

41f5c176

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

kex-y committed 3 years ago

4048a9be

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

vihdzp committed 3 years ago

d56a9bc2

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

tb65536 committed 3 years ago

1e560a67

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

YaelDillies committed 3 years ago

24e3b5f5

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

CBirkbeck committed 3 years ago

0fd99294

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

eric-wieser committed 3 years ago

750ca956

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

eric-wieser committed 3 years ago

8836a42d

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

Sebastian-Monnet committed 3 years ago

9e288527

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

YaelDillies committed 3 years ago

bab039fb

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

jjaassoonn committed 3 years ago

9c2f6ebe

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

tb65536 committed 3 years ago

ef25c4ca

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

kbuzzard committed 3 years ago

9facd190

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

eric-wieser committed 3 years ago

0d6fb8a7

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

alexjbest committed 3 years ago

c4a34136

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

vihdzp committed 3 years ago

55d1f3e8

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

eric-wieser committed 3 years ago

5d405e2a

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

eric-wieser committed 3 years ago

bc9dda83

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

eric-wieser committed 3 years ago

94e9bb55

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

PatrickMassot committed 3 years ago

b8d176e0

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

leanprover-community-bot committed 3 years ago

1f6a2e9d

feat(data/equiv/basic): lemmas about composition with equivalences (#10693)

antoinelab01 committed 3 years ago

2a3ecad0

chore(order/well_founded_set): golf two proofs (#12529)

eric-wieser committed 3 years ago

d69cda1e

feat(set_theory/cardinal_ordinal): `#(list α) ≤ max ω (#α)` (#12519)

vihdzp committed 3 years ago

709a3b70

Newer Older