leanprover-community/mathlib3

Pull Requests Commits

feat(tactic/ext): support rintro patterns in `ext` (#12875)

digama0 committed 4 years ago

debdd909

chore(data/int/basic): remove some `eq.mpr`s from `int.induction_on'` (#12873)

eric-wieser committed 4 years ago

8e50164d

fix(ring_theory/algebraic): Make `is_transcendental_of_subsingleton` fully general (#12870)

vihdzp committed 4 years ago

ae695782

feat(data/{nat, real}/sqrt): Some simple facts about square roots (#12851)

khwilson committed 4 years ago

706a824c

feat(group_theory/order_of_element): finite orderness is closed under mul (#12750)

Julian committed 4 years ago

ec434b75

feat(analysis/locally_convex): characterize the natural bornology in terms of seminorms (#12721)

mcdoll committed 4 years ago

c705d414

chore(algebra/category/*): simp lemmas for of_hom (#12638)

kim-em committed 4 years ago

cbd1e98c

feat(data/complex/basic): `#ℂ = 𝔠` (#12871)

vihdzp committed 4 years ago

7967128a

chore(data/{lists,multiset}/*): More dot notation (#12876)

YaelDillies committed 4 years ago

584ae9db

feat(order/hom/*): more superclass instances for `order_iso_class` (#12889)

YaelDillies committed 4 years ago

e6205190

refactor(order/upper_lower): Use `⨆` rather than `Sup` (#12644)

YaelDillies committed 4 years ago

3b8d217c

feat(category_theory/abelian): right derived functor in abelian category with enough injectives (#12810)

jjaassoonn committed 4 years ago

cd942870

refactor(algebraic_geometry/*): rename structure sheaf to `Spec.structure_sheaf` (#12785)

jjaassoonn committed 4 years ago

84a438e2

chore(model_theory/terms_and_formulas): `realize_to_prenex` (#12884)

awainverse committed 4 years ago

16fb8e26

feat(ring_theory/polynomial/basic): the isomorphism between `R[a]/I[a]` and `(R/I[X])/(f mod I)` for `a` a root of polynomial `f` and `I` and ideal of `R` (#12646)

Paul-Lez committed 4 years ago

64472d74

chore(docs/references): Remove duplicate key (#12901)

YaelDillies committed 4 years ago

91263102

feat(model_theory/terms_and_formulas): Make `Theory.model` a class (#12867)

awainverse committed 4 years ago

2308b53c

feat(algebra/homology/quasi_iso): 2-out-of-3 property (#12898)

joelriou committed 4 years ago

92f26698

feat(linear_algebra/matrix): add variants of the existing `det_units_conj` lemmas (#12881)

eric-wieser committed 4 years ago

11a365de

chore(data/nat/prime): golf nat.dvd_prime_pow (#12886)

Ruben-VandeVelde committed 4 years ago

c60bfca9

feat(set_theory/ordinal): Small iff cardinality less than `cardinal.univ` (#12887)

awainverse committed 4 years ago

d711d2a2

feat(model_theory/*): Language equivalences (#12837)

awainverse committed 4 years ago

3838b852

feat(order/concept): Concept lattices (#12286)

YaelDillies committed 4 years ago

f7905f0c

feat(*): `has_repr` instances for `option`-like types (#11282)

YaelDillies committed 4 years ago

b226b4b6

feat(algebra/{group,module}/ulift): Missing `ulift` instances (#12879)

YaelDillies committed 4 years ago

980185a1

feat(algebra/subalgebra/basic): Missing scalar instances (#12874)

YaelDillies committed 4 years ago

6a55ba89

feat(order/filter/basic): `filter` is a `coframe` (#12872)

YaelDillies committed 4 years ago

52159408

refactor(order/hom/complete_lattice): Fix the definition of `frame_hom` (#12855)

YaelDillies committed 4 years ago

1f470163

feat(data/finset/pointwise): Missing operations (#12865)

YaelDillies committed 4 years ago

d5861954

feat(analysis/calculus): define `diff_on_int_cont` (#12688)

urkud committed 4 years ago

28eb06f9

Newer Older