leanprover-community / leanprover-community/physlib
Module doc-string improvements
Open
Nobody has claimed this yet.
- Dominant language
- Lean
- Stars
- 749
- Forks
- 189
- Avg merge
- 1d 21h
- Merged PRs (30d)
- 75
Description
This issue is to track which module-doc strings are good and which need improving.
If a doc-string for a module is already 'good', please tick it off here, otherwise feel free to improve it.
Doc-string module improvements
Classical mechanics
- PhysLean.ClassicalMechanics.Basic
- PhysLean.ClassicalMechanics.EulerLagrange
- PhysLean.ClassicalMechanics.HamiltonsEquations
- #738
- PhysLean.ClassicalMechanics.HarmonicOscillator.Solution
- PhysLean.ClassicalMechanics.Mass.MassUnit
- PhysLean.ClassicalMechanics.VectorFields
- PhysLean.ClassicalMechanics.WaveEquation.Basic
- PhysLean.ClassicalMechanics.WaveEquation.HarmonicWave
Condensed matter
Cosmology
Electromagnetism
- PhysLean.Electromagnetism.Basic
- PhysLean.Electromagnetism.Charge.ChargeUnit
- #723
- PhysLean.Electromagnetism.Electrostatics.OneDimension.PointParticle
- PhysLean.Electromagnetism.Electrostatics.OneDimension.Vacuum
- PhysLean.Electromagnetism.Electrostatics.TreeDimension.PointParticle
- PhysLean.Electromagnetism.FieldStrength.Basic
- PhysLean.Electromagnetism.FieldStrength.Derivative
- PhysLean.Electromagnetism.Homogeneous
- PhysLean.Electromagnetism.LorentzAction
- PhysLean.Electromagnetism.MaxwellEquations
- PhysLean.Electromagnetism.Wave
Mathematics
- PhysLean.Mathematics.Calculus.AdjFDeriv
- PhysLean.Mathematics.Calculus.Divergence
- PhysLean.Mathematics.DataStructures.FourTree.Basic
- PhysLean.Mathematics.DataStructures.FourTree.UniqueMap
- PhysLean.Mathematics.DataStructures.Matrix.LieTrace
- PhysLean.Mathematics.Distribution.Basic
- PhysLean.Mathematics.Distribution.OfBounded
- PhysLean.Mathematics.Distribution.PowMul
- PhysLean.Mathematics.FDerivCurry
- PhysLean.Mathematics.Fin
- PhysLean.Mathematics.Fin.Involutions
- PhysLean.Mathematics.Geometry.Metric.PseudoRiemannian.Defs
- PhysLean.Mathematics.Geometry.Metric.Riemannian.Defs
- PhysLean.Mathematics.InnerProductSpace.Adjoint
- PhysLean.Mathematics.InnerProductSpace.Basic
- PhysLean.Mathematics.InnerProductSpace.Calculus
- PhysLean.Mathematics.LinearMaps
- PhysLean.Mathematics.List
- PhysLean.Mathematics.List.InsertIdx
- PhysLean.Mathematics.List.InsertionSort
- PhysLean.Mathematics.PiTensorProduct
- PhysLean.Mathematics.RatComplexNum
- PhysLean.Mathematics.SO3.Basic
- PhysLean.Mathematics.SchurTriangulation
- PhysLean.Mathematics.SpecialFunctions.PhysHermite
- PhysLean.Mathematics.Trigonometry.Tanh
- PhysLean.Mathematics.VariationalCalculus.Basic
- PhysLean.Mathematics.VariationalCalculus.HasVarAdjDeriv
- PhysLean.Mathematics.VariationalCalculus.HasVarAdjoint
- PhysLean.Mathematics.VariationalCalculus.HasVarGradient
- PhysLean.Mathematics.VariationalCalculus.IsLocalizedfunctionTransform
- PhysLean.Mathematics.VariationalCalculus.IsTestFunction
Meta
- PhysLean.Meta.AllFilePaths
- PhysLean.Meta.Basic
- PhysLean.Meta.Informal.Basic
- PhysLean.Meta.Informal.Post
- PhysLean.Meta.Informal.SemiFormal
- PhysLean.Meta.Linters.Sorry
- PhysLean.Meta.Notes.Basic
- PhysLean.Meta.Notes.HTMLNote
- PhysLean.Meta.Notes.NoteFile
- PhysLean.Meta.Notes.ToHTML
- PhysLean.Meta.Remark.Basic
- PhysLean.Meta.Remark.Properties
- PhysLean.Meta.TODO.Basic
- PhysLean.Meta.TransverseTactics
Optics
Particles
- PhysLean.Particles.BeyondTheStandardModel.GeorgiGlashow.Basic
- PhysLean.Particles.BeyondTheStandardModel.PatiSalam.Basic
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Basic
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.FamilyMaps
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.NoGrav.Basic
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.Basic
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.DimSevenPlane
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.FamilyMaps
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Permutations
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.BMinusL
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.Basic
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.BoundPlaneDim
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.FamilyMaps
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.HyperCharge
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.PlaneNonSols
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.QuadSol
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.QuadSolToSol
- PhysLean.Particles.BeyondTheStandardModel.Spin10.Basic
- PhysLean.Particles.BeyondTheStandardModel.TwoHDM.Basic
- PhysLean.Particles.BeyondTheStandardModel.TwoHDM.GaugeOrbits
- PhysLean.Particles.FlavorPhysics.CKMMatrix.Basic
- PhysLean.Particles.FlavorPhysics.CKMMatrix.Invariants
- PhysLean.Particles.FlavorPhysics.CKMMatrix.PhaseFreedom
- PhysLean.Particles.FlavorPhysics.CKMMatrix.Relations
- PhysLean.Particles.FlavorPhysics.CKMMatrix.Rows
- PhysLean.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
- PhysLean.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
- PhysLean.Particles.StandardModel.AnomalyCancellation.Basic
- PhysLean.Particles.StandardModel.AnomalyCancellation.FamilyMaps
- PhysLean.Particles.StandardModel.AnomalyCancellation.NoGrav.Basic
- PhysLean.Particles.StandardModel.AnomalyCancellation.NoGrav.One.Lemmas
- PhysLean.Particles.StandardModel.AnomalyCancellation.NoGrav.One.LinearParameterization
- PhysLean.Particles.StandardModel.AnomalyCancellation.Permutations
- PhysLean.Particles.StandardModel.Basic
- PhysLean.Particles.StandardModel.HiggsBoson.Basic
- PhysLean.Particles.StandardModel.HiggsBoson.GaugeAction
- PhysLean.Particles.StandardModel.HiggsBoson.PointwiseInnerProd
- PhysLean.Particles.StandardModel.HiggsBoson.Potential
- PhysLean.Particles.StandardModel.Representations
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.B3
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Basic
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.HyperCharge
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.LineY3B3
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.Basic
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.PlaneWithY3B3
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.ToSols
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Permutations
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Y3
- PhysLean.Particles.SuperSymmetry.SU5.Charges.AllowsTerm
- PhysLean.Particles.SuperSymmetry.SU5.Charges.Basic
- PhysLean.Particles.SuperSymmetry.SU5.Charges.Completions
- PhysLean.Particles.SuperSymmetry.SU5.Charges.Map
- PhysLean.Particles.SuperSymmetry.SU5.Charges.MinimalSuperSet
- PhysLean.Particles.SuperSymmetry.SU5.Charges.MinimallyAllowsTerm.Basic
- PhysLean.Particles.SuperSymmetry.SU5.Charges.MinimallyAllowsTerm.FinsetTerms
- PhysLean.Particles.SuperSymmetry.SU5.Charges.MinimallyAllowsTerm.OfFinset
- PhysLean.Particles.SuperSymmetry.SU5.Charges.OfFieldLabel
- PhysLean.Particles.SuperSymmetry.SU5.Charges.OfPotentialTerm
- PhysLean.Particles.SuperSymmetry.SU5.Charges.PhenoClosed
- PhysLean.Particles.SuperSymmetry.SU5.Charges.PhenoConstrained
- PhysLean.Particles.SuperSymmetry.SU5.Charges.U1U1
- PhysLean.Particles.SuperSymmetry.SU5.Charges.Yukawa
- PhysLean.Particles.SuperSymmetry.SU5.Charges.ZMod
- PhysLean.Particles.SuperSymmetry.SU5.FieldLabels
- PhysLean.Particles.SuperSymmetry.SU5.Potential
QFT
- PhysLean.QFT.AnomalyCancellation.Basic
- PhysLean.QFT.AnomalyCancellation.GroupActions
- PhysLean.QFT.PerturbationTheory.CreateAnnihilate
- PhysLean.QFT.PerturbationTheory.FeynmanDiagrams.Basic
- PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.Basic
- PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.Grading
- PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.NormTimeOrder
- PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.NormalOrder
- PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute
- PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder
- PhysLean.QFT.PerturbationTheory.FieldSpecification.Basic
- PhysLean.QFT.PerturbationTheory.FieldSpecification.CrAnFieldOp
- PhysLean.QFT.PerturbationTheory.FieldSpecification.CrAnSection
- PhysLean.QFT.PerturbationTheory.FieldSpecification.Filters
- PhysLean.QFT.PerturbationTheory.FieldSpecification.NormalOrder
- PhysLean.QFT.PerturbationTheory.FieldSpecification.TimeOrder
- PhysLean.QFT.PerturbationTheory.FieldStatistics.Basic
- PhysLean.QFT.PerturbationTheory.FieldStatistics.ExchangeSign
- PhysLean.QFT.PerturbationTheory.FieldStatistics.OfFinset
- PhysLean.QFT.PerturbationTheory.Koszul.KoszulSign
- PhysLean.QFT.PerturbationTheory.Koszul.KoszulSignInsert
- PhysLean.QFT.PerturbationTheory.WickAlgebra.Basic
- PhysLean.QFT.PerturbationTheory.WickAlgebra.Grading
- PhysLean.QFT.PerturbationTheory.WickAlgebra.NormalOrder.Basic
- PhysLean.QFT.PerturbationTheory.WickAlgebra.NormalOrder.Lemmas
- PhysLean.QFT.PerturbationTheory.WickAlgebra.NormalOrder.WickContractions
- PhysLean.QFT.PerturbationTheory.WickAlgebra.StaticWickTerm
- PhysLean.QFT.PerturbationTheory.WickAlgebra.StaticWickTheorem
- PhysLean.QFT.PerturbationTheory.WickAlgebra.SuperCommute
- PhysLean.QFT.PerturbationTheory.WickAlgebra.TimeContraction
- PhysLean.QFT.PerturbationTheory.WickAlgebra.TimeOrder
- PhysLean.QFT.PerturbationTheory.WickAlgebra.Universality
- PhysLean.QFT.PerturbationTheory.WickAlgebra.WickTerm
- PhysLean.QFT.PerturbationTheory.WickAlgebra.WicksTheorem
- PhysLean.QFT.PerturbationTheory.WickAlgebra.WicksTheoremNormal
- PhysLean.QFT.PerturbationTheory.WickContraction.Basic
- PhysLean.QFT.PerturbationTheory.WickContraction.Card
- PhysLean.QFT.PerturbationTheory.WickContraction.Erase
- PhysLean.QFT.PerturbationTheory.WickContraction.ExtractEquiv
- PhysLean.QFT.PerturbationTheory.WickContraction.InsertAndContract
- PhysLean.QFT.PerturbationTheory.WickContraction.InsertAndContractNat
- PhysLean.QFT.PerturbationTheory.WickContraction.Involutions
- PhysLean.QFT.PerturbationTheory.WickContraction.IsFull
- PhysLean.QFT.PerturbationTheory.WickContraction.Join
- PhysLean.QFT.PerturbationTheory.WickContraction.Perm
- PhysLean.QFT.PerturbationTheory.WickContraction.Sign.Basic
- PhysLean.QFT.PerturbationTheory.WickContraction.Sign.InsertNone
- PhysLean.QFT.PerturbationTheory.WickContraction.Sign.InsertSome
- PhysLean.QFT.PerturbationTheory.WickContraction.Sign.Join
- PhysLean.QFT.PerturbationTheory.WickContraction.Singleton
- PhysLean.QFT.PerturbationTheory.WickContraction.StaticContract
- PhysLean.QFT.PerturbationTheory.WickContraction.SubContraction
- PhysLean.QFT.PerturbationTheory.WickContraction.TimeCond
- PhysLean.QFT.PerturbationTheory.WickContraction.TimeContract
- PhysLean.QFT.PerturbationTheory.WickContraction.Uncontracted
- PhysLean.QFT.PerturbationTheory.WickContraction.UncontractedList
- PhysLean.QFT.QED.AnomalyCancellation.Basic
- PhysLean.QFT.QED.AnomalyCancellation.BasisLinear
- PhysLean.QFT.QED.AnomalyCancellation.ConstAbs
- PhysLean.QFT.QED.AnomalyCancellation.Even.BasisLinear
- PhysLean.QFT.QED.AnomalyCancellation.Even.LineInCubic
- PhysLean.QFT.QED.AnomalyCancellation.Even.Parameterization
- PhysLean.QFT.QED.AnomalyCancellation.LineInPlaneCond
- PhysLean.QFT.QED.AnomalyCancellation.LowDim.One
- PhysLean.QFT.QED.AnomalyCancellation.LowDim.Three
- PhysLean.QFT.QED.AnomalyCancellation.LowDim.Two
- PhysLean.QFT.QED.AnomalyCancellation.Odd.BasisLinear
- PhysLean.QFT.QED.AnomalyCancellation.Odd.LineInCubic
- PhysLean.QFT.QED.AnomalyCancellation.Odd.Parameterization
- PhysLean.QFT.QED.AnomalyCancellation.Permutations
- PhysLean.QFT.QED.AnomalyCancellation.Sorts
- PhysLean.QFT.QED.AnomalyCancellation.VectorLike
Quantum mechanics
- PhysLean.QuantumMechanics.FiniteTarget.Basic
- PhysLean.QuantumMechanics.FiniteTarget.HilbertSpace
- PhysLean.QuantumMechanics.OneDimension.GeneralPotential.Basic
- PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Basic
- PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Completeness
- PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
- PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.TISE
- PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Basic
- PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Gaussians
- PhysLean.QuantumMechanics.OneDimension.HilbertSpace.PlaneWaves
- PhysLean.QuantumMechanics.OneDimension.HilbertSpace.PositionStates
- PhysLean.QuantumMechanics.OneDimension.HilbertSpace.SchwartzSubmodule
- PhysLean.QuantumMechanics.OneDimension.Operators.Commutation
- PhysLean.QuantumMechanics.OneDimension.Operators.Momentum
- PhysLean.QuantumMechanics.OneDimension.Operators.Parity
- PhysLean.QuantumMechanics.OneDimension.Operators.Position
- PhysLean.QuantumMechanics.OneDimension.Operators.Unbounded
- PhysLean.QuantumMechanics.OneDimension.ReflectionlessPotential.Basic
- PhysLean.QuantumMechanics.PlanckConstant
Relativity
- PhysLean.Relativity.Bispinors.Basic
- PhysLean.Relativity.CliffordAlgebra
- PhysLean.Relativity.LorentzAlgebra.Basic
- PhysLean.Relativity.LorentzAlgebra.Basis
- PhysLean.Relativity.LorentzAlgebra.ExponentialMap
- PhysLean.Relativity.LorentzGroup.Basic
- PhysLean.Relativity.LorentzGroup.Boosts.Apply
- PhysLean.Relativity.LorentzGroup.Boosts.Basic
- PhysLean.Relativity.LorentzGroup.Boosts.Generalized
- PhysLean.Relativity.LorentzGroup.Orthochronous.Basic
- PhysLean.Relativity.LorentzGroup.Proper
- PhysLean.Relativity.LorentzGroup.Restricted.Basic
- PhysLean.Relativity.LorentzGroup.Restricted.FromBoostRotation
- PhysLean.Relativity.LorentzGroup.Rotations
- PhysLean.Relativity.LorentzGroup.ToVector
- PhysLean.Relativity.MinkowskiMatrix
- PhysLean.Relativity.PauliMatrices.AsTensor
- PhysLean.Relativity.PauliMatrices.Basic
- PhysLean.Relativity.PauliMatrices.CliffordAlgebra
- PhysLean.Relativity.PauliMatrices.Relations
- PhysLean.Relativity.PauliMatrices.SelfAdjoint
- PhysLean.Relativity.PauliMatrices.ToTensor
- PhysLean.Relativity.SL2C.Basic
- PhysLean.Relativity.SL2C.SelfAdjoint
- PhysLean.Relativity.Special.ProperTime
- PhysLean.Relativity.Special.TwinParadox.Basic
- PhysLean.Relativity.Tensors.Basic
- PhysLean.Relativity.Tensors.Color.Basic
- PhysLean.Relativity.Tensors.Color.Discrete
- PhysLean.Relativity.Tensors.Color.Lift
- PhysLean.Relativity.Tensors.ComplexTensor.Basic
- PhysLean.Relativity.Tensors.ComplexTensor.Lemmas
- PhysLean.Relativity.Tensors.ComplexTensor.Matrix.Pre
- PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Basic
- PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Lemmas
- PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Pre
- PhysLean.Relativity.Tensors.ComplexTensor.OfRat
- PhysLean.Relativity.Tensors.ComplexTensor.Units.Basic
- PhysLean.Relativity.Tensors.ComplexTensor.Units.Pre
- PhysLean.Relativity.Tensors.ComplexTensor.Units.Symm
- PhysLean.Relativity.Tensors.ComplexTensor.Vector.Pre.Basic
- PhysLean.Relativity.Tensors.ComplexTensor.Vector.Pre.Contraction
- PhysLean.Relativity.Tensors.ComplexTensor.Vector.Pre.Modules
- PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Basic
- PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Contraction
- PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Metric
- PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Modules
- PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Two
- PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Unit
- PhysLean.Relativity.Tensors.Constructors
- PhysLean.Relativity.Tensors.Contraction.Basic
- PhysLean.Relativity.Tensors.Contraction.Basis
- PhysLean.Relativity.Tensors.Contraction.Products
- PhysLean.Relativity.Tensors.Contraction.Pure
- PhysLean.Relativity.Tensors.Dual
- PhysLean.Relativity.Tensors.Elab
- PhysLean.Relativity.Tensors.Evaluation
- PhysLean.Relativity.Tensors.MetricTensor
- PhysLean.Relativity.Tensors.OfInt
- PhysLean.Relativity.Tensors.Product
- PhysLean.Relativity.Tensors.RealTensor.Basic
- PhysLean.Relativity.Tensors.RealTensor.Derivative
- PhysLean.Relativity.Tensors.RealTensor.Matrix.Pre
- PhysLean.Relativity.Tensors.RealTensor.Metrics.Basic
- PhysLean.Relativity.Tensors.RealTensor.Metrics.Pre
- PhysLean.Relativity.Tensors.RealTensor.ToComplex
- PhysLean.Relativity.Tensors.RealTensor.Units.Pre
- PhysLean.Relativity.Tensors.RealTensor.Vector.Basic
- PhysLean.Relativity.Tensors.RealTensor.Vector.Causality.Basic
- PhysLean.Relativity.Tensors.RealTensor.Vector.Causality.LightLike
- PhysLean.Relativity.Tensors.RealTensor.Vector.Causality.TimeLike
- PhysLean.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct
- PhysLean.Relativity.Tensors.RealTensor.Vector.Pre.Basic
- PhysLean.Relativity.Tensors.RealTensor.Vector.Pre.Contraction
- PhysLean.Relativity.Tensors.RealTensor.Vector.Pre.Modules
- PhysLean.Relativity.Tensors.RealTensor.Velocity.Basic
- PhysLean.Relativity.Tensors.TensorSpecies.Basic
- PhysLean.Relativity.Tensors.Tensorial
- PhysLean.Relativity.Tensors.UnitTensor
SpaceAndTime
- PhysLean.SpaceAndTime.Space.Basic
- PhysLean.SpaceAndTime.Space.Distributions
- PhysLean.SpaceAndTime.Space.LengthUnit
- PhysLean.SpaceAndTime.Space.SpaceStruct
- PhysLean.SpaceAndTime.Space.VectorIdentities
- PhysLean.SpaceAndTime.SpaceTime.Basic
- PhysLean.SpaceAndTime.SpaceTime.TimeSlice
- PhysLean.SpaceAndTime.Time.Basic
- PhysLean.SpaceAndTime.Time.TimeMan
- PhysLean.SpaceAndTime.Time.TimeTransMan
- PhysLean.SpaceAndTime.Time.TimeUnit
StatisticalMechanics
- PhysLean.StatisticalMechanics.BoltzmannConstant
- PhysLean.StatisticalMechanics.CanonicalEnsemble.Basic
- PhysLean.StatisticalMechanics.CanonicalEnsemble.Finite
- PhysLean.StatisticalMechanics.CanonicalEnsemble.TwoState
StringTheory
- PhysLean.StringTheory.Basic
- PhysLean.StringTheory.FTheory.SU5.Basic
- PhysLean.StringTheory.FTheory.SU5.Charges.AnomalyFree
- PhysLean.StringTheory.FTheory.SU5.Charges.OfRationalSection
- PhysLean.StringTheory.FTheory.SU5.Charges.Viable
- PhysLean.StringTheory.FTheory.SU5.Fluxes.Basic
- PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.ChiralIndices
- PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.Completeness
- PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.Elems
- PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.ToList
- PhysLean.StringTheory.FTheory.SU5.Quanta.Basic
- PhysLean.StringTheory.FTheory.SU5.Quanta.FiveQuanta
- PhysLean.StringTheory.FTheory.SU5.Quanta.IsViable
- PhysLean.StringTheory.FTheory.SU5.Quanta.TenQuanta
Thermodynamics
- PhysLean.Thermodynamics.Basic
- PhysLean.Thermodynamics.Temperature.Basic
- PhysLean.Thermodynamics.Temperature.TemperatureUnits
Units
- PhysLean.Units.Basic
- PhysLean.Units.Examples
- PhysLean.Units.FDeriv
- PhysLean.Units.Integral
- PhysLean.Units.WithDim.Area
- PhysLean.Units.WithDim.Basic
- PhysLean.Units.WithDim.Energy
- PhysLean.Units.WithDim.Mass
- PhysLean.Units.WithDim.Momentum
- PhysLean.Units.WithDim.Pressure
- PhysLean.Units.WithDim.Speed
- PhysLean.Units.WithDim.Velocity
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Choose one unchecked module from the checklist, such as PhysLean.ClassicalMechanics.Basic or PhysLean.Meta.Basic, and read its existing module doc-string in the linked .lean file. Improve the documentation where needed, confirm it accurately describes the module, and tick that entry when complete.
Written by the indexing model from the issue text.
Assessment
- Domain
- documentation
- Issue type
- Documentation
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100