leanprover-community/mathlib

Pull Requests Commits

feat(data/real/{e,}nnreal): images and preimages of `ord_connected` sets (#15483)

urkud committed 3 years ago

b60a2703

feat(data/list/basic): last_reverse (#15482)

pechersky committed 3 years ago

ed513f85

doc(set_theory/cardinal/basic): tweak documentation (#15480)

vihdzp committed 3 years ago

a641e1b6

feat(algebra/order/monoid): add `one_lt_mul_iff`/`add_pos_iff` (#15458)

urkud committed 3 years ago

5c062ff9

feat(topology/instances/nnreal): add `can_lift C(X, ℝ) C(X, ℝ≥0)` (#15446)

urkud committed 3 years ago

fc2d456a

chore(logic/equiv/fin): golf, avoid `norm_num` (#15442)

urkud committed 3 years ago

1a30610a

feat(order/hom/basic): `order_iso` of `rel_iso (<) (<)` (#15432)

vihdzp committed 3 years ago

3b19e7ee

feat(number_theory/legendre_symbol/*): redefine quadratic characters as `mul_char`s (#15418)

MichaelStollBayreuth committed 3 years ago

1627d8d7

feat(ring_theory/I_filtration): I-filtrations of modules. (#15333)

erdOne committed 3 years ago

ea330542

feat(topology): basic simplification lemmas for `continuous_map`s (#15102)

ralvrz committed 3 years ago

1d937ddf

feat(algebra/lie/cartan_subalgebra): characterise Cartan subalgebras as limiting values of upper central series (#14179)

ocfnash committed 3 years ago

691c0035

feat(topology/sets/closeds): The coframe of closed sets (#15338)

YaelDillies committed 3 years ago

e82fbd32

feat(geometry/euclidean/oriented_angle): `continuous_at_oangle` (#15463)

jsm28 committed 3 years ago

e3f47f2b

chore(set_theory/ordinal/arithmetic): improve `enum_iso` def-eq (#15454)

vihdzp committed 3 years ago

09ff086c

A finite orthonormal family is an orthonormal

ADedecker committed 3 years ago

6c61ebb7

feat(geometry/manifold/metrizable): metrizability of a manifold (#15437)

urkud committed 3 years ago

2067c013

feat(order/lattice): Congruence lemmas for `⊔` and `⊓` (#15439)

YaelDillies committed 3 years ago

5b4425ae

Unused argument

ADedecker committed 3 years ago

774e2447

`linear_equiv.of_eq` as a `linear_isometry_equiv`

ADedecker committed 3 years ago

90722c0e

feat(data/set/finite): set.finite.induction_on' (#15444)

berndlosert committed 3 years ago

87fc6828

chore(linear_algebra/matrix): Use the new matrix notation in most places (#15306)

eric-wieser committed 3 years ago

65ec5990

Define positive operators

ADedecker committed 3 years ago

a27ba1b4

feat(linear_algebra/matrix/charpoly): Coefficients of the characteristic polynomial falls in the ideal power. (#15459)

erdOne committed 3 years ago

9745b093

feat(algebra/group/with_one): units of a group with zero is isomorphic to the group (#15403)

Multramate committed 3 years ago

f19c6153

chore(set_theory/zfc): better def-eqs (#15210)

vihdzp committed 3 years ago

98f747f8

feat(category_theory/preadditive): projective iff coyoneda.obj preserves epimorphisms (#14832)

TwoFX committed 3 years ago

d84d1af4

refactor(analysis/inner_product_space/pi_L2): change `std_orthonormal_basis` to type `orthonormal_basis` (#12253)

hrmacbeth committed 3 years ago

5b774133

feat(data/set/countable): protect lemmas (#15415)

vihdzp committed 3 years ago

6379d39e

feat(algebraic_geometry): Intersection of affine open can be covered by common basic opens (#11649)

erdOne committed 3 years ago

621cf7f2

doc(undergrad): add unitary and orthogonal group (#15456)

mcdoll committed 3 years ago

bb08977c

Newer Older