Commit 2023-08-04 22:34 c4679d7b

View on Github →

chore: tidy various files (#6291)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

Modified Mathlib/Data/Finset/Lattice.lean

added theorem Finset.isGLB_iff_isLeast

added theorem Finset.isGLB_mem

added theorem Finset.isLUB_iff_isGreatest

added theorem Finset.isLUB_mem

deleted theorem Finset.is_glb_iff_is_least

deleted theorem Finset.is_glb_mem

deleted theorem Finset.is_lub_iff_is_greatest

deleted theorem Finset.is_lub_mem

Modified Mathlib/Data/Fintype/Card.lean

added def Equiv.ofLeftInverseOfCardLE

deleted def Equiv.ofLeftInverseOfCardLe

added def Equiv.ofRightInverseOfCardLE

deleted def Equiv.ofRightInverseOfCardLe

deleted theorem Fintype.card_Prop

added theorem Fintype.card_prop

added theorem Function.Embedding.isEmpty_of_card_lt

deleted theorem Function.Embedding.is_empty_of_card_lt

added def Function.Embedding.truncOfCardLE

deleted def Function.Embedding.truncOfCardLe

added theorem isEmpty_fintype

deleted theorem is_empty_fintype

Modified Mathlib/Data/List/Perm.lean

Modified Mathlib/Data/Real/EReal.lean

Modified Mathlib/FieldTheory/PrimitiveElement.lean

Modified Mathlib/GroupTheory/Congruence.lean

Modified Mathlib/LinearAlgebra/Basis.lean

added theorem Basis.coe_mkFinConsOfLE

deleted theorem Basis.coe_mkFinConsOfLe

added def Basis.groupSMul

added theorem Basis.groupSMul_apply

added theorem Basis.groupSMul_span_eq_top

deleted def Basis.groupSmul

deleted theorem Basis.groupSmul_apply

deleted theorem Basis.groupSmul_span_eq_top

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

Modified Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean

added theorem rieszContentAux_image_nonempty

deleted theorem riesz_content_aux_image_nonempty

Modified Mathlib/ModelTheory/Semantics.lean

added theorem FirstOrder.Language.BoundedFormula.realize_castLE_of_eq

deleted theorem FirstOrder.Language.BoundedFormula.realize_castLe_of_eq

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

Modified Mathlib/Order/Interval.lean

modified theorem NonemptyInterval.coe_coeHom

Modified Mathlib/Order/SuccPred/LinearLocallyFinite.lean

Modified Mathlib/Order/WithBot.lean

Modified Mathlib/RingTheory/GradedAlgebra/Radical.lean

Modified Mathlib/RingTheory/WittVector/Frobenius.lean

deleted theorem WittVector.frobeniusPoly_zMod

added theorem WittVector.frobeniusPoly_zmod

Modified Mathlib/RingTheory/WittVector/StructurePolynomial.lean

Modified Mathlib/RingTheory/WittVector/WittPolynomial.lean

deleted theorem wittPolynomial_zMod_self

added theorem wittPolynomial_zmod_self

Modified Mathlib/Topology/Sheaves/PUnit.lean

deleted theorem TopCat.Presheaf.isSheaf_on_pUnit_iff_isTerminal

deleted theorem TopCat.Presheaf.isSheaf_on_pUnit_of_isTerminal

added theorem TopCat.Presheaf.isSheaf_on_punit_iff_isTerminal

added theorem TopCat.Presheaf.isSheaf_on_punit_of_isTerminal

Modified Mathlib/Topology/Sheaves/Skyscraper.lean